eliminated gif dir;
authorwenzelm
Wed, 09 Feb 2000 12:29:03 +0100
changeset 8218 6c4bec5cd2ac
parent 8217 dc3b8cdbb816
child 8219 504689622489
eliminated gif dir;
lib/Tools/usedir
lib/html/index1.html
lib/html/index2.html
--- 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
--- 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 @@
 
 <body>
 
-<center><img src="gif/isabelle.gif" alt="Isabelle"></center>
+<center><img src="isabelle.gif" alt="Isabelle"></center>
 
 <p>
 
--- 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 @@
 
 <body>
 
-<center><img src="../gif/isabelle.gif" alt="Isabelle"></center>
+<center><img src="../isabelle.gif" alt="Isabelle"></center>
 
 <p>