Fix

benedikt-schesch · May 27, 2024 · b91f693 · b91f693
1 parent 7237d4d
commit b91f693
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/run.sh b/run.sh
@@ -125,6 +125,7 @@ if [ -d "repos" ]; then
 fi
 
 # Delete .workdir
+chmod -R +w .workdir
 rm -rf .workdir
 
 python3 src/python/delete_cache_placeholders.py \

diff --git a/src/python/latex_output.py b/src/python/latex_output.py
@@ -164,12 +164,17 @@ def latex_def(name, value) -> str:
     "tools": [
         "gitmerge_ort",
         "gitmerge_ort_ignorespace",
-        "gitmerge_ort_adjacent",
-        "gitmerge_ort_imports",
-        "gitmerge_ort_imports_ignorespace",
         "git_hires_merge",
         "spork",
         "intellimerge",
+        "plumelib_ort",
+        "plumelib_ort_ignorespace",
+        "plumelib_ort_adjacent",
+        "plumelib_ort_adjacent_ignorespace",
+        "plumelib_ort_imports",
+        "plumelib_ort_imports_ignorespace",
+        "plumelib_ort_version_number",
+        "plumelib_ort_version_number_ignorespace",
     ],
 }