Removed cp / mkdir commands for graph browser files.
--- 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