Exclude irrelevant files from the diff output

[briantist]

Any change in the docs results in changes to .js and .inv files that aren't useful to see. It'd be best to exclude them from the diff output, especially since the size of the output that we can display is limited by github API limits. In anything but the smallest of collections, the output from those seems large enough to exceed the maximum and will cause truncation (although these files tend to be at the end, so at least the truncation will most likely trim this output first).

We're using git diff --no-index to generate this output. --no-index is used because neither directory being compared is a git repo. git diff has a way to filter files, and the relevant filter should be something like this:

':(exclude)**/*.js' ':(exclude)**/*.inv'

However, the filter only works without --no-index.

One thing we can do when generating the diff output is to make one or both of the generated docs sets into a repo with git init and then do the comparison. This will need some experimentation to get the procedure right, and should probably be configurable via the action's inputs.

[felixfontein]

Alternatively, one can simply delete the corresponding files in both directories before doing the diff.

[briantist]

Alternatively, one can simply delete the corresponding files in both directories before doing the diff.

yes, that too! as long as we're careful to do so after the artifact is uploaded ;)