# HG changeset patch # User berghofe # Date 960373003 -7200 # Node ID 81096680966363172a2a66010a304e5533e8b046 # Parent 17c5edf1706b23358b3448378eff9981f70486a1 Removed cp / mkdir commands for graph browser files. diff -r 17c5edf1706b -r 810966809663 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