Removed cp / mkdir commands for graph browser files.
authorberghofe
Wed, 07 Jun 2000 12:16:43 +0200
changeset 9047 810966809663
parent 9046 17c5edf1706b
child 9048 3add5cfc89c2
Removed cp / mkdir commands for graph browser files.
lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Jun 07 12:15:26 2000 +0200
+++ b/lib/Tools/usedir	Wed Jun 07 12:16:43 2000 +0200
@@ -109,12 +109,6 @@
   mkdir -p $ISABELLE_BROWSER_INFO
   cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
   cp $ISABELLE_HOME/lib/html/index.html $ISABELLE_BROWSER_INFO/index.html
-
-  mkdir -p $ISABELLE_BROWSER_INFO/graph
-  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
-  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
-  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
-  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
 fi