src/Doc/Main/document/build
changeset 73739 3e44f8c3f059
parent 73738 d701bd96e323
child 73740 c46ff0efa1ce
equal deleted inserted replaced
73738:d701bd96e323 73739:3e44f8c3f059
     1 #!/usr/bin/env bash
       
     2 
       
     3 set -e
       
     4 
       
     5 FORMAT="$1"
       
     6 VARIANT="$2"
       
     7 
       
     8 isabelle latex -o "$FORMAT"
       
     9 isabelle latex -o "$FORMAT"
       
    10