compile script change

tahiat · Apr 2, 2024 · 5309116 · 5309116
1 parent b6ba451
commit 5309116
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/check_compilation.sh b/check_compilation.sh
@@ -21,7 +21,11 @@ cd ISSUES || exit 1
 for target in $issue_ids; do
     echo "Target = ${target}"
 
-    cd "${target}/output/" || exit 1
+    cd "${target}/output/"
+    if [ $? -eq 1 ]; then
+      compile_status_json="$compile_status_json\n  \"$target\": \"FAIL\","
+      continue
+    fi
     # check if any directory exists inside output. If no directory there, specimin failed on the input target
     # in that case, ignoring it.
     directory_count="$(find ./ -mindepth 1 -type d | wc -l)"