sagemath · vbraun · May 2, 2024 · Oct 21, 2023 · Oct 22, 2023 · Nov 1, 2023
diff --git a/.ci/create-changes-html.sh b/.ci/create-changes-html.sh
@@ -51,7 +51,7 @@ diffParagraphs.forEach(paragraph => {
 EOF
 echo '</head>' >> CHANGES.html
 echo '<body>' >> CHANGES.html
-(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- *.html) > diff.txt
+(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- "*.html") > diff.txt
 python3 - << EOF
 import os, re, html
 with open('diff.txt', 'r') as f:

diff --git a/.ci/docker-exec-script.sh b/.ci/docker-exec-script.sh
@@ -0,0 +1,14 @@
+#!/bin/sh -x
+if [ $# -lt 3 ]; then
+    echo >&2 "usage: docker-exec-script.sh CONTAINER WORKDIR [VAR=VALUE...] SCRIPT"
+    exit 1
+fi
+CONTAINER=$1
+WORKDIR=$2
+shift 2
+(echo "cd \"$WORKDIR\"";
+ while [ $# -gt 1 ]; do
+     echo "export \"$1\""
+     shift
+ done;
+ cat "$1") | docker exec -i $CONTAINER bash -ex