allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
authorwenzelm
Fri, 17 Aug 2012 11:42:05 +0200
changeset 48837 d1d806a42c91
parent 48836 90a0af19004c
child 48838 623ba165d059
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira; clarified spaces in file names -- ISABELLE_HOME is non-critical after abolishment of "make";
lib/Tools/version
lib/scripts/getsettings
--- a/lib/Tools/version	Fri Aug 17 11:37:14 2012 +0200
+++ b/lib/Tools/version	Fri Aug 17 11:42:05 2012 +0200
@@ -60,7 +60,7 @@
   if [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
   else
-    ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
+    "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
   fi
 else
   echo 'unidentified repository version'    # filled in automatically!
--- a/lib/scripts/getsettings	Fri Aug 17 11:37:14 2012 +0200
+++ b/lib/scripts/getsettings	Fri Aug 17 11:42:05 2012 +0200
@@ -34,11 +34,6 @@
 fi
 
 export ISABELLE_HOME
-if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
-then
-  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
-  echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
-fi
 
 #key executables
 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
@@ -58,7 +53,7 @@
 
 #Isabelle distribution identifier -- filled in automatically!
 ISABELLE_ID=""
-ISABELLE_IDENTIFIER=""
+[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
 
 #sometimes users put strange things in here ...
 unset ENV