src/Doc/Nitpick/document/build
changeset 56534 3ff16a7f0b2e
parent 53498 05313b45a5ae
child 62589 b5783412bfed
equal deleted inserted replaced
56533:cd8b6d849b6a 56534:3ff16a7f0b2e
     4 
     4 
     5 FORMAT="$1"
     5 FORMAT="$1"
     6 VARIANT="$2"
     6 VARIANT="$2"
     7 
     7 
     8 "$ISABELLE_TOOL" logo Nitpick
     8 "$ISABELLE_TOOL" logo Nitpick
     9 
       
    10 cp "$ISABELLE_HOME/src/Doc/iman.sty" .
       
    11 cp "$ISABELLE_HOME/src/Doc/manual.bib" .
       
    12 
       
    13 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
     9 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
    14 
    10