jj/.github/scripts
Ilya Grigoriev 043f786fbf website: Stop mike from always changing sitemaps.xml.gz
Originally, my motivation was to try again to get `mike` to not push empty
commits (which this should do). I'm now reconsidering this, since *not* pushing
empty commits will make the output of the CI job a little harder to read. If
this becomes an issue, I  might even add `--allow-empty` to the `mike`
invocations later.

A more important motivation is that even for a 400-byte file, changing it for
every PR blows up the size of the repo eventually.

The cause for the changes to this file was that `gzip` stores a timestamp
inside the `.gz` file.
2023-11-06 17:10:27 -08:00
..
docs-build-deploy website: Stop mike from always changing sitemaps.xml.gz 2023-11-06 17:10:27 -08:00