src/Doc/prepare_document
changeset 73731 a1ef2589c33f
parent 73725 cd9afbd0ccb9
child 73733 b13b2c1d419e
equal deleted inserted replaced
73730:2f023b2b0e1e 73731:a1ef2589c33f
     6 
     6 
     7 isabelle latex -o "$FORMAT"
     7 isabelle latex -o "$FORMAT"
     8 isabelle latex -o bbl
     8 isabelle latex -o bbl
     9 [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
     9 [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
    10 isabelle latex -o "$FORMAT"
    10 isabelle latex -o "$FORMAT"
    11 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
       
    12 isabelle latex -o "$FORMAT"
    11 isabelle latex -o "$FORMAT"