allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
authorwenzelm
Fri Aug 17 11:42:05 2012 +0200 (2012-08-17)
changeset 48837d1d806a42c91
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
     1.1 --- a/lib/Tools/version	Fri Aug 17 11:37:14 2012 +0200
     1.2 +++ b/lib/Tools/version	Fri Aug 17 11:42:05 2012 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4    if [ -n "$ISABELLE_ID" ]; then
     1.5      echo "$ISABELLE_ID"
     1.6    else
     1.7 -    ${HG:-hg} id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
     1.8 +    "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
     1.9    fi
    1.10  else
    1.11    echo 'unidentified repository version'    # filled in automatically!
     2.1 --- a/lib/scripts/getsettings	Fri Aug 17 11:37:14 2012 +0200
     2.2 +++ b/lib/scripts/getsettings	Fri Aug 17 11:42:05 2012 +0200
     2.3 @@ -34,11 +34,6 @@
     2.4  fi
     2.5  
     2.6  export ISABELLE_HOME
     2.7 -if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
     2.8 -then
     2.9 -  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
    2.10 -  echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    2.11 -fi
    2.12  
    2.13  #key executables
    2.14  ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    2.15 @@ -58,7 +53,7 @@
    2.16  
    2.17  #Isabelle distribution identifier -- filled in automatically!
    2.18  ISABELLE_ID=""
    2.19 -ISABELLE_IDENTIFIER=""
    2.20 +[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    2.21  
    2.22  #sometimes users put strange things in here ...
    2.23  unset ENV