Re: [PATCH] add a script to diff rendered documentation
From: brian m. carlson <hidden>
Date: 2018-08-05 20:49:40
On Fri, Aug 03, 2018 at 04:52:05PM -0400, Jeff King wrote:
I wrote this up for my own use after our discussion in [1]. I'm not sure if it's too ugly for inclusion, or if it might be helpful to others. I've only just written it, but my plan is to try to run it on anything I submit to check the formatting. So it _seems_ useful and appears to work, but only after a few minutes of playing with it. :)
I think this would indeed be valuable. Junio seemed to indicate that he would use it, and I would certainly use it as well.
quoted hunk ↗ jump to hunk
diff --git a/Documentation/doc-diff b/Documentation/doc-diff new file mode 100755 index 0000000000..61deb2579e --- /dev/null +++ b/Documentation/doc-diff@@ -0,0 +1,100 @@ +#!/bin/sh + +OPTIONS_SPEC="\ +doc-diff <from> <to> [-- diff options] +-- +j parallel argument to pass to make +f force rebuild; do not rely on cached results +" +SUBDIRECTORY_OK=1 +. "$(git --exec-path)/git-sh-setup" + +parallel=8
I'm not sure -j8 is a great default. There are still a lot of two-core/four-thread machines out there, such as my laptop (from 2016). Maybe we should default this to 1 unless -j is provided, like make does. -- brian m. carlson: Houston, Texas, US OpenPGP: https://keybase.io/bk2204
Attachments
- signature.asc [application/pgp-signature] 867 bytes