etc/options
changeset 74840 4faf0ec33cbf
parent 74827 c1b5d6e6ff74
child 76041 4a1330addb4e
--- a/etc/options	Wed Nov 24 21:04:39 2021 +0100
+++ b/etc/options	Wed Nov 24 22:57:33 2021 +0100
@@ -23,6 +23,8 @@
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
 option document_heading_prefix : string = "isamarkup" (standard)
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
+option document_comment_latex : bool = false
+  -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"