Re: [PATCH] add a script to diff rendered documentation

["brian m. carlson" <sandals@crustytoothpaste.net>]

[-- Attachment #1: Type: text/plain, Size: 1297 bytes --]

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.

> 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 867 bytes --]