Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Ensure that output is written within session directory.
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Achim D. Brucker 2023-03-06 23:23:23 +01:00
parent 3670d30ddf
commit 1229db1432
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Isabelle_DOF-Unit-Tests/TestKit.thy
View File

@ -58,9 +58,8 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark
val file = {path = Path.make [oid' ^ "_snippet.tex"],
pos = @{here},
content = Bytes.string strg}
val _ = Generated_Files.write_file (Path.make ["latex_test"])
file
val dir = Path.append (Resources.master_directory thy) (Path.make ["latex_test"])
val _ = Generated_Files.write_file dir file
val _ = writeln (strg)
in () end \<comment> \<open>important observation: thy is not modified.
This implies that several text block can be