more robust invocation of hg;
authorwenzelm
Sat, 27 Mar 2021 17:05:36 +0100
changeset 73479 6e20976d58f5
parent 73478 1be70e3de751
child 73480 0e880b793db1
more robust invocation of hg;
Admin/cronjob/plain_identify
Admin/cronjob/self_update
Admin/lib/Tools/churn
Admin/lib/Tools/churn_pie
--- a/Admin/cronjob/plain_identify	Sat Mar 27 15:56:49 2021 +0100
+++ b/Admin/cronjob/plain_identify	Sat Mar 27 17:05:36 2021 +0100
@@ -19,15 +19,15 @@
   local SOURCE="$2"
   mkdir -p "$REPOS_DIR"
   if [ ! -d "$REPOS_DIR/$NAME" ]; then
-    hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
+    "${HG:-hg}" clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
   fi
 }
 
 function identify_repos ()
 {
   local NAME="$1"
-  hg pull -R "$REPOS_DIR/$NAME" -q
-  local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
+  "${HG:-hg}" pull -R "$REPOS_DIR/$NAME" -q
+  local ID="$("${HG:-hg}" tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
   echo "$NAME version: $ID"
 }
 
--- a/Admin/cronjob/self_update	Sat Mar 27 15:56:49 2021 +0100
+++ b/Admin/cronjob/self_update	Sat Mar 27 17:05:36 2021 +0100
@@ -11,7 +11,7 @@
 mkdir -p run log
 
 {
-  hg -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2
-  hg -R isabelle update -C || echo "self_update update failed" >&2
+  "${HG:-hg}" -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2
+  "${HG:-hg}" -R isabelle update -C || echo "self_update update failed" >&2
   isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2
 } > run/self_update.out
--- a/Admin/lib/Tools/churn	Sat Mar 27 15:56:49 2021 +0100
+++ b/Admin/lib/Tools/churn	Sat Mar 27 17:05:36 2021 +0100
@@ -9,4 +9,4 @@
 
 cd "$(dirname "$ALIAS")"
 
-hg churn --aliases "$ALIAS" "$@"
+"${HG:-hg}" churn --aliases "$ALIAS" "$@"
--- a/Admin/lib/Tools/churn_pie	Sat Mar 27 15:56:49 2021 +0100
+++ b/Admin/lib/Tools/churn_pie	Sat Mar 27 17:05:36 2021 +0100
@@ -11,4 +11,4 @@
 
 cd "$(dirname "$ALIAS")"
 
-hg churn --aliases "$ALIAS" | "$SCRIPT" "$@"
+"${HG:-hg}" churn --aliases "$ALIAS" | "$SCRIPT" "$@"