# HG changeset patch
# User wenzelm
# Date 1616861136 -3600
# Node ID 6e20976d58f5e94a8b7592865207716ad00612bb
# Parent  1be70e3de7513a9a9e05ba3d4850bcb53628edc5
more robust invocation of hg;

diff -r 1be70e3de751 -r 6e20976d58f5 Admin/cronjob/plain_identify
--- 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"
 }
 
diff -r 1be70e3de751 -r 6e20976d58f5 Admin/cronjob/self_update
--- 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
diff -r 1be70e3de751 -r 6e20976d58f5 Admin/lib/Tools/churn
--- 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" "$@"
diff -r 1be70e3de751 -r 6e20976d58f5 Admin/lib/Tools/churn_pie
--- 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" "$@"