--- a/bin/isabelle Wed Nov 22 21:38:26 2000 +0100
+++ b/bin/isabelle Wed Nov 22 21:41:39 2000 +0100
@@ -9,9 +9,9 @@
## settings
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
-ISABELLE_HOME=$(dirname "$0")/..
+ISABELLE_HOME="$(dirname "$0")/.."
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
{ echo "$PRG probably not called from its original place!"; exit 2; }
--- a/bin/isatool Wed Nov 22 21:38:26 2000 +0100
+++ b/bin/isatool Wed Nov 22 21:41:39 2000 +0100
@@ -10,9 +10,9 @@
## settings
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
-ISABELLE_HOME=$(dirname "$0")/..
+ISABELLE_HOME="$(dirname "$0")/.."
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
{ echo "$PRG probably not called from its original place!"; exit 2; }
--- a/build Wed Nov 22 21:38:26 2000 +0100
+++ b/build Wed Nov 22 21:41:39 2000 +0100
@@ -14,10 +14,10 @@
## settings
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
export THIS_IS_ISABELLE_BUILD=true
-ISABELLE_HOME=$(dirname "$0")
+ISABELLE_HOME="$(dirname "$0")"
. "$ISABELLE_HOME/lib/scripts/getsettings" || \
{ echo "$PRG probably not called from its original place!"; exit 2; }
@@ -164,9 +164,7 @@
# build it
SECONDS=0
-DATE=$(date)
-HOST=$(hostname)
-echo "Started at $DATE ($HOST)"
+echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
for L in $MAKE_LOGICS
do
--- a/configure Wed Nov 22 21:38:26 2000 +0100
+++ b/configure Wed Nov 22 21:41:39 2000 +0100
@@ -8,7 +8,7 @@
## patch scripts
-cd `dirname "$0"`
+cd "`dirname "$0"`"
if bash -c :
then
--- a/lib/Tools/browser Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/browser Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: Isabelle graph browser
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/doc Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/doc Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: view Isabelle documentation
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/document Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/document Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: prepare theory session document
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/expandshort Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/expandshort Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: expand shorthand goal commands
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixclasimp Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixclasimp Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixdatatype Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixdatatype Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixdots Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixdots Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixgoal Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixgoal Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixseq Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixseq Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/fixsome Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/fixsome Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/getenv Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/getenv Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/installfonts Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/installfonts Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: install symbol fonts on the current X11 server
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/latex Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/latex Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: run LaTeX (and related tools)
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/logo Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/logo Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: create an instance of the Isabelle logo
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/make Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/make Wed Nov 22 21:41:39 2000 +0100
@@ -7,7 +7,7 @@
# DESCRIPTION: Isabelle make utility
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/makeall Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/makeall Wed Nov 22 21:41:39 2000 +0100
@@ -13,7 +13,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
@@ -30,11 +30,7 @@
[ "$1" = "-?" ] && usage
-
-SECONDS=0
-DATE=$(date)
-HOST=$(hostname)
-echo "Started at $DATE ($HOST)"
+echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
for L in $ALL_LOGICS
do
--- a/lib/Tools/mkdir Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/mkdir Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/nonascii Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/nonascii Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/unsymbolize Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/unsymbolize Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{
--- a/lib/Tools/usedir Wed Nov 22 21:38:26 2000 +0100
+++ b/lib/Tools/usedir Wed Nov 22 21:41:39 2000 +0100
@@ -9,7 +9,7 @@
## diagnostics
-PRG=$(basename "$0")
+PRG="$(basename "$0")"
function usage()
{