Omit excessive quotes
This commit is contained in:
parent
7772c73aaa
commit
5a8c438c41
|
@ -67,8 +67,8 @@ object DOF_Mkroot
|
||||||
|
|
||||||
File.write(root_path,
|
File.write(root_path,
|
||||||
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
|
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
|
||||||
options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """"
|
options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """
|
||||||
+ quote(DOF.implode_ontologies(ontologies)) + """", dof_template = """ + quote(template)
|
+ quote(DOF.implode_ontologies(ontologies)) + """, dof_template = """ + quote(template)
|
||||||
+ """, document_comment_latex = true]
|
+ """, document_comment_latex = true]
|
||||||
(*theories [document = false]
|
(*theories [document = false]
|
||||||
A
|
A
|
||||||
|
|
Loading…
Reference in New Issue