tuned;
authorwenzelm
Wed Nov 22 21:41:39 2000 +0100 (2000-11-22)
changeset 10511efb3428c9879
parent 10510 d243553849ec
child 10512 d34192966cd8
tuned;
bin/isabelle
bin/isatool
build
configure
lib/Tools/browser
lib/Tools/doc
lib/Tools/document
lib/Tools/expandshort
lib/Tools/fixclasimp
lib/Tools/fixdatatype
lib/Tools/fixdots
lib/Tools/fixgoal
lib/Tools/fixseq
lib/Tools/fixsome
lib/Tools/getenv
lib/Tools/installfonts
lib/Tools/latex
lib/Tools/logo
lib/Tools/make
lib/Tools/makeall
lib/Tools/mkdir
lib/Tools/nonascii
lib/Tools/unsymbolize
lib/Tools/usedir
     1.1 --- a/bin/isabelle	Wed Nov 22 21:38:26 2000 +0100
     1.2 +++ b/bin/isabelle	Wed Nov 22 21:41:39 2000 +0100
     1.3 @@ -9,9 +9,9 @@
     1.4  
     1.5  ## settings
     1.6  
     1.7 -PRG=$(basename "$0")
     1.8 +PRG="$(basename "$0")"
     1.9  
    1.10 -ISABELLE_HOME=$(dirname "$0")/..
    1.11 +ISABELLE_HOME="$(dirname "$0")/.."
    1.12  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    1.13    { echo "$PRG probably not called from its original place!"; exit 2; }
    1.14  
     2.1 --- a/bin/isatool	Wed Nov 22 21:38:26 2000 +0100
     2.2 +++ b/bin/isatool	Wed Nov 22 21:41:39 2000 +0100
     2.3 @@ -10,9 +10,9 @@
     2.4  
     2.5  ## settings
     2.6  
     2.7 -PRG=$(basename "$0")
     2.8 +PRG="$(basename "$0")"
     2.9  
    2.10 -ISABELLE_HOME=$(dirname "$0")/..
    2.11 +ISABELLE_HOME="$(dirname "$0")/.."
    2.12  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    2.13    { echo "$PRG probably not called from its original place!"; exit 2; }
    2.14  
     3.1 --- a/build	Wed Nov 22 21:38:26 2000 +0100
     3.2 +++ b/build	Wed Nov 22 21:41:39 2000 +0100
     3.3 @@ -14,10 +14,10 @@
     3.4  
     3.5  ## settings
     3.6  
     3.7 -PRG=$(basename "$0")
     3.8 +PRG="$(basename "$0")"
     3.9  
    3.10  export THIS_IS_ISABELLE_BUILD=true
    3.11 -ISABELLE_HOME=$(dirname "$0")
    3.12 +ISABELLE_HOME="$(dirname "$0")"
    3.13  . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    3.14    { echo "$PRG probably not called from its original place!"; exit 2; }
    3.15  
    3.16 @@ -164,9 +164,7 @@
    3.17  # build it
    3.18  
    3.19  SECONDS=0
    3.20 -DATE=$(date)
    3.21 -HOST=$(hostname)
    3.22 -echo "Started at $DATE ($HOST)"
    3.23 +echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
    3.24  
    3.25  for L in $MAKE_LOGICS
    3.26  do
     4.1 --- a/configure	Wed Nov 22 21:38:26 2000 +0100
     4.2 +++ b/configure	Wed Nov 22 21:41:39 2000 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  ## patch scripts
     4.6  
     4.7 -cd `dirname "$0"`
     4.8 +cd "`dirname "$0"`"
     4.9  
    4.10  if bash -c :
    4.11  then
     5.1 --- a/lib/Tools/browser	Wed Nov 22 21:38:26 2000 +0100
     5.2 +++ b/lib/Tools/browser	Wed Nov 22 21:41:39 2000 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  # DESCRIPTION: Isabelle graph browser
     5.5  
     5.6  
     5.7 -PRG=$(basename "$0")
     5.8 +PRG="$(basename "$0")"
     5.9  
    5.10  function usage()
    5.11  {
     6.1 --- a/lib/Tools/doc	Wed Nov 22 21:38:26 2000 +0100
     6.2 +++ b/lib/Tools/doc	Wed Nov 22 21:41:39 2000 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  # DESCRIPTION: view Isabelle documentation
     6.5  
     6.6  
     6.7 -PRG=$(basename "$0")
     6.8 +PRG="$(basename "$0")"
     6.9  
    6.10  function usage()
    6.11  {
     7.1 --- a/lib/Tools/document	Wed Nov 22 21:38:26 2000 +0100
     7.2 +++ b/lib/Tools/document	Wed Nov 22 21:41:39 2000 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  # DESCRIPTION: prepare theory session document
     7.5  
     7.6  
     7.7 -PRG=$(basename "$0")
     7.8 +PRG="$(basename "$0")"
     7.9  
    7.10  function usage()
    7.11  {
     8.1 --- a/lib/Tools/expandshort	Wed Nov 22 21:38:26 2000 +0100
     8.2 +++ b/lib/Tools/expandshort	Wed Nov 22 21:41:39 2000 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  # DESCRIPTION: expand shorthand goal commands
     8.5  
     8.6  
     8.7 -PRG=$(basename "$0")
     8.8 +PRG="$(basename "$0")"
     8.9  
    8.10  function usage()
    8.11  {
     9.1 --- a/lib/Tools/fixclasimp	Wed Nov 22 21:38:26 2000 +0100
     9.2 +++ b/lib/Tools/fixclasimp	Wed Nov 22 21:41:39 2000 +0100
     9.3 @@ -9,7 +9,7 @@
     9.4  
     9.5  ## diagnostics
     9.6  
     9.7 -PRG=$(basename "$0")
     9.8 +PRG="$(basename "$0")"
     9.9  
    9.10  function usage()
    9.11  {
    10.1 --- a/lib/Tools/fixdatatype	Wed Nov 22 21:38:26 2000 +0100
    10.2 +++ b/lib/Tools/fixdatatype	Wed Nov 22 21:41:39 2000 +0100
    10.3 @@ -9,7 +9,7 @@
    10.4  
    10.5  ## diagnostics
    10.6  
    10.7 -PRG=$(basename "$0")
    10.8 +PRG="$(basename "$0")"
    10.9  
   10.10  function usage()
   10.11  {
    11.1 --- a/lib/Tools/fixdots	Wed Nov 22 21:38:26 2000 +0100
    11.2 +++ b/lib/Tools/fixdots	Wed Nov 22 21:41:39 2000 +0100
    11.3 @@ -9,7 +9,7 @@
    11.4  
    11.5  ## diagnostics
    11.6  
    11.7 -PRG=$(basename "$0")
    11.8 +PRG="$(basename "$0")"
    11.9  
   11.10  function usage()
   11.11  {
    12.1 --- a/lib/Tools/fixgoal	Wed Nov 22 21:38:26 2000 +0100
    12.2 +++ b/lib/Tools/fixgoal	Wed Nov 22 21:41:39 2000 +0100
    12.3 @@ -9,7 +9,7 @@
    12.4  
    12.5  ## diagnostics
    12.6  
    12.7 -PRG=$(basename "$0")
    12.8 +PRG="$(basename "$0")"
    12.9  
   12.10  function usage()
   12.11  {
    13.1 --- a/lib/Tools/fixseq	Wed Nov 22 21:38:26 2000 +0100
    13.2 +++ b/lib/Tools/fixseq	Wed Nov 22 21:41:39 2000 +0100
    13.3 @@ -9,7 +9,7 @@
    13.4  
    13.5  ## diagnostics
    13.6  
    13.7 -PRG=$(basename "$0")
    13.8 +PRG="$(basename "$0")"
    13.9  
   13.10  function usage()
   13.11  {
    14.1 --- a/lib/Tools/fixsome	Wed Nov 22 21:38:26 2000 +0100
    14.2 +++ b/lib/Tools/fixsome	Wed Nov 22 21:41:39 2000 +0100
    14.3 @@ -9,7 +9,7 @@
    14.4  
    14.5  ## diagnostics
    14.6  
    14.7 -PRG=$(basename "$0")
    14.8 +PRG="$(basename "$0")"
    14.9  
   14.10  function usage()
   14.11  {
    15.1 --- a/lib/Tools/getenv	Wed Nov 22 21:38:26 2000 +0100
    15.2 +++ b/lib/Tools/getenv	Wed Nov 22 21:41:39 2000 +0100
    15.3 @@ -9,7 +9,7 @@
    15.4  
    15.5  ## diagnostics
    15.6  
    15.7 -PRG=$(basename "$0")
    15.8 +PRG="$(basename "$0")"
    15.9  
   15.10  function usage()
   15.11  {
    16.1 --- a/lib/Tools/installfonts	Wed Nov 22 21:38:26 2000 +0100
    16.2 +++ b/lib/Tools/installfonts	Wed Nov 22 21:41:39 2000 +0100
    16.3 @@ -7,7 +7,7 @@
    16.4  # DESCRIPTION: install symbol fonts on the current X11 server
    16.5  
    16.6  
    16.7 -PRG=$(basename "$0")
    16.8 +PRG="$(basename "$0")"
    16.9  
   16.10  function usage()
   16.11  {
    17.1 --- a/lib/Tools/latex	Wed Nov 22 21:38:26 2000 +0100
    17.2 +++ b/lib/Tools/latex	Wed Nov 22 21:41:39 2000 +0100
    17.3 @@ -7,7 +7,7 @@
    17.4  # DESCRIPTION: run LaTeX (and related tools)
    17.5  
    17.6  
    17.7 -PRG=$(basename "$0")
    17.8 +PRG="$(basename "$0")"
    17.9  
   17.10  function usage()
   17.11  {
    18.1 --- a/lib/Tools/logo	Wed Nov 22 21:38:26 2000 +0100
    18.2 +++ b/lib/Tools/logo	Wed Nov 22 21:41:39 2000 +0100
    18.3 @@ -7,7 +7,7 @@
    18.4  # DESCRIPTION: create an instance of the Isabelle logo
    18.5  
    18.6  
    18.7 -PRG=$(basename "$0")
    18.8 +PRG="$(basename "$0")"
    18.9  
   18.10  function usage()
   18.11  {
    19.1 --- a/lib/Tools/make	Wed Nov 22 21:38:26 2000 +0100
    19.2 +++ b/lib/Tools/make	Wed Nov 22 21:41:39 2000 +0100
    19.3 @@ -7,7 +7,7 @@
    19.4  # DESCRIPTION: Isabelle make utility
    19.5  
    19.6  
    19.7 -PRG=$(basename "$0")
    19.8 +PRG="$(basename "$0")"
    19.9  
   19.10  function usage()
   19.11  {
    20.1 --- a/lib/Tools/makeall	Wed Nov 22 21:38:26 2000 +0100
    20.2 +++ b/lib/Tools/makeall	Wed Nov 22 21:41:39 2000 +0100
    20.3 @@ -13,7 +13,7 @@
    20.4  
    20.5  ## diagnostics
    20.6  
    20.7 -PRG=$(basename "$0")
    20.8 +PRG="$(basename "$0")"
    20.9  
   20.10  function usage()
   20.11  {
   20.12 @@ -30,11 +30,7 @@
   20.13  
   20.14  [ "$1" = "-?" ] && usage
   20.15  
   20.16 -
   20.17 -SECONDS=0
   20.18 -DATE=$(date)
   20.19 -HOST=$(hostname)
   20.20 -echo "Started at $DATE ($HOST)"
   20.21 +echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   20.22  
   20.23  for L in $ALL_LOGICS
   20.24  do
    21.1 --- a/lib/Tools/mkdir	Wed Nov 22 21:38:26 2000 +0100
    21.2 +++ b/lib/Tools/mkdir	Wed Nov 22 21:41:39 2000 +0100
    21.3 @@ -9,7 +9,7 @@
    21.4  
    21.5  ## diagnostics
    21.6  
    21.7 -PRG=$(basename "$0")
    21.8 +PRG="$(basename "$0")"
    21.9  
   21.10  function usage()
   21.11  {
    22.1 --- a/lib/Tools/nonascii	Wed Nov 22 21:38:26 2000 +0100
    22.2 +++ b/lib/Tools/nonascii	Wed Nov 22 21:41:39 2000 +0100
    22.3 @@ -9,7 +9,7 @@
    22.4  
    22.5  ## diagnostics
    22.6  
    22.7 -PRG=$(basename "$0")
    22.8 +PRG="$(basename "$0")"
    22.9  
   22.10  function usage()
   22.11  {
    23.1 --- a/lib/Tools/unsymbolize	Wed Nov 22 21:38:26 2000 +0100
    23.2 +++ b/lib/Tools/unsymbolize	Wed Nov 22 21:41:39 2000 +0100
    23.3 @@ -9,7 +9,7 @@
    23.4  
    23.5  ## diagnostics
    23.6  
    23.7 -PRG=$(basename "$0")
    23.8 +PRG="$(basename "$0")"
    23.9  
   23.10  function usage()
   23.11  {
    24.1 --- a/lib/Tools/usedir	Wed Nov 22 21:38:26 2000 +0100
    24.2 +++ b/lib/Tools/usedir	Wed Nov 22 21:41:39 2000 +0100
    24.3 @@ -9,7 +9,7 @@
    24.4  
    24.5  ## diagnostics
    24.6  
    24.7 -PRG=$(basename "$0")
    24.8 +PRG="$(basename "$0")"
    24.9  
   24.10  function usage()
   24.11  {