etc/options
changeset 72578 3e8395f9093a
parent 72300 9f07e961a2b0
child 72675 cc1347c8c804
equal deleted inserted replaced
72577:77b51733ffdf 72578:3e8395f9093a
     6   -- "generate theory browser information"
     6   -- "generate theory browser information"
     7 
     7 
     8 option document : string = ""
     8 option document : string = ""
     9   -- "build document in given format: pdf, dvi, false"
     9   -- "build document in given format: pdf, dvi, false"
    10 option document_output : string = ""
    10 option document_output : string = ""
    11   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
    11   -- "document output directory"
       
    12 option document_output_sources : bool = true
       
    13   -- "copy generated sources into document output directory"
    12 option document_variants : string = "document"
    14 option document_variants : string = "document"
    13   -- "alternative document variants (separated by colons)"
    15   -- "alternative document variants (separated by colons)"
    14 option document_tags : string = ""
    16 option document_tags : string = ""
    15   -- "default command tags (separated by commas)"
    17   -- "default command tags (separated by commas)"
    16 
    18