#61 remove rich.xml

zerocracy · Jul 23, 2024 · a3b900b · a3b900b
1 parent 7446e0b
commit a3b900b
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/entry.sh b/entry.sh
@@ -84,7 +84,10 @@ done <<< "${INPUT_OPTIONS}"
     --max-cycles 1 \
     "${options[@]}" \
     "${SELF}/judges/" "${INPUT_FACTBASE}"
-"${JUDGES}" "${gopts[@]}" print --format xml "${INPUT_FACTBASE}" "${INPUT_OUTPUT}/${name}.rich.xml"
+"${JUDGES}" "${gopts[@]}" print \
+    --format xml \
+    "${INPUT_FACTBASE}" \
+    "${INPUT_OUTPUT}/${name}.rich.xml"
 
 # Build a summary HTML.
 css=$(cat "${SELF}/target/css/main.css")
@@ -101,3 +104,4 @@ java -jar "${SELF}/target/saxon.jar" \
     "css=${css}" \
     "js=${js}"
 echo "HTML generated at ${html}"
+rm "${INPUT_OUTPUT}/${name}.rich.xml"