Add header comment to document script

Co-authored-by: Richard van der Hoff <1389908+richvdh@users.noreply.github.com>
pull/2226/head
Johannes Marbach 1 month ago committed by GitHub
parent 9ca00d2119
commit 4dc44c1021
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

@ -1,5 +1,6 @@
#!/bin/bash
#
# Download the KaTeX fonts and CSS, and copy them into `static`.
set -e
root=$(git rev-parse --show-toplevel)

Loading…
Cancel
Save