# HG changeset patch # User wenzelm # Date 950095743 -3600 # Node ID 6c4bec5cd2ac6023f41967ca6958b9822b1d5fbc # Parent dc3b8cdbb816688a24436c94d6428c9a49347998 eliminated gif dir; diff -r dc3b8cdbb816 -r 6c4bec5cd2ac lib/Tools/usedir --- a/lib/Tools/usedir Wed Feb 09 12:28:44 2000 +0100 +++ b/lib/Tools/usedir Wed Feb 09 12:29:03 2000 +0100 @@ -102,8 +102,7 @@ if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then - mkdir -p $ISABELLE_BROWSER_INFO/gif - cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif + cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html mkdir -p $ISABELLE_BROWSER_INFO/graph diff -r dc3b8cdbb816 -r 6c4bec5cd2ac lib/html/index1.html --- a/lib/html/index1.html Wed Feb 09 12:28:44 2000 +0100 +++ b/lib/html/index1.html Wed Feb 09 12:29:03 2000 +0100 @@ -4,7 +4,7 @@ -
Isabelle
+
Isabelle

diff -r dc3b8cdbb816 -r 6c4bec5cd2ac lib/html/index2.html --- a/lib/html/index2.html Wed Feb 09 12:28:44 2000 +0100 +++ b/lib/html/index2.html Wed Feb 09 12:29:03 2000 +0100 @@ -4,7 +4,7 @@ -

Isabelle
+
Isabelle