From b91f6937b5b26eb253e06539f972bcb2b6fb94a1 Mon Sep 17 00:00:00 2001 From: Benedikt Schesch Date: Mon, 27 May 2024 13:34:01 -0700 Subject: [PATCH] Fix --- run.sh | 1 + src/python/latex_output.py | 11 ++++++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/run.sh b/run.sh index c2389bd03c..0ff3955fc7 100755 --- 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 index ca1952c196..7ce24202c7 100755 --- 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", ], }