From 4dc44c102158fc8ee4702e29e241e71702d02862 Mon Sep 17 00:00:00 2001 From: Johannes Marbach Date: Thu, 30 Oct 2025 15:43:51 +0100 Subject: [PATCH] Add header comment to document script Co-authored-by: Richard van der Hoff <1389908+richvdh@users.noreply.github.com> --- scripts/download-katex-assets.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/download-katex-assets.sh b/scripts/download-katex-assets.sh index 68ee1bcb..9c555b6b 100755 --- a/scripts/download-katex-assets.sh +++ b/scripts/download-katex-assets.sh @@ -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)