doc-src/prepare_document
changeset 48971 5a4bcf466156
equal deleted inserted replaced
48970:8be091776e93 48971:5a4bcf466156
       
     1 #!/bin/bash
       
     2 
       
     3 set -e
       
     4 
       
     5 FORMAT="$1"
       
     6 
       
     7 "$ISABELLE_TOOL" latex -o sty
       
     8 cp "$ISABELLE_HOME/doc-src/pdfsetup.sty" .
       
     9 
       
    10 "$ISABELLE_TOOL" latex -o "$FORMAT"
       
    11 "$ISABELLE_TOOL" latex -o bbl
       
    12 [ -f root.idx ] && "$ISABELLE_HOME/doc-src/sedindex" root
       
    13 "$ISABELLE_TOOL" latex -o "$FORMAT"
       
    14 [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
       
    15 "$ISABELLE_TOOL" latex -o "$FORMAT"
       
    16