lib/Tools/usedir
changeset 3844 7704dc8997ed
parent 3747 cd9b6c86926c
child 3848 97bb3ff3c771
equal deleted inserted replaced
3843:162f95673705 3844:7704dc8997ed
    73 
    73 
    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/*.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/html/index1.html $ISABELLE_BROWSER_INFO/index.html
    80   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
    80   mkdir -p $ISABELLE_BROWSER_INFO/graph
    81   mkdir -p $ISABELLE_BROWSER_INFO/graph
    81   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
    82   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
    83   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
    83   mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
    84   mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities