equal
deleted
inserted
replaced
74 # prepare directories for html and graph output |
74 # prepare directories for html and graph output |
75 |
75 |
76 if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then |
76 if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then |
77 mkdir -p $ISABELLE_BROWSER_INFO/gif |
77 mkdir -p $ISABELLE_BROWSER_INFO/gif |
78 cp $ISABELLE_HOME/lib/images/*arrow.gif $ISABELLE_BROWSER_INFO/gif |
78 cp $ISABELLE_HOME/lib/images/*arrow.gif $ISABELLE_BROWSER_INFO/gif |
79 cp $ISABELLE_HOME/lib/logo/isabelle_transparent.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif |
79 cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif |
80 cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html |
80 cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html |
81 mkdir -p $ISABELLE_BROWSER_INFO/graph |
81 mkdir -p $ISABELLE_BROWSER_INFO/graph |
82 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html |
82 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html |
83 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser |
83 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser |
84 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities |
84 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities |