Delete useless option in ICFEM 2022 paper ROOT

- document_comment_latex=true is required for lipics style but the paper uses lncs style
2022-04-20 10:32:42 +02:00 · 2022-04-20 10:32:42 +02:00 · 9770f8c332
parent 8aba7f272a
commit 9770f8c332
1 changed files with 1 additions and 2 deletions
--- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT
+++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT
@ -1,6 +1,5 @@
 session "2021-ITP-PMTI" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof,
-    document_comment_latex = true]
+  options [document = pdf, document_output = "output", document_build = dof]
  theories
    "paper"
  document_files