lib/Tools/usedir
changeset 8241 a55484a9b19f
parent 8218 6c4bec5cd2ac
child 8359 124ad46105dd
equal deleted inserted replaced
8240:87e08624e209 8241:a55484a9b19f
   100 
   100 
   101 # prepare browser info dir
   101 # prepare browser info dir
   102 
   102 
   103 if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
   103 if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
   104 
   104 
       
   105   mkdir -p $ISABELLE_BROWSER_INFO
   105   cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
   106   cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
   106   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
   107   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
   107 
   108 
   108   mkdir -p $ISABELLE_BROWSER_INFO/graph
   109   mkdir -p $ISABELLE_BROWSER_INFO/graph
   109   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
   110   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html