Re-enable test0001 in github CI script.

GaloisInc · Jan 19, 2021 · a7eee69 · a7eee69
1 parent 535e29d
commit a7eee69
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -170,7 +170,7 @@ install_system_deps() {
 test_dist() {
   find_java
   pushd intTests
-  for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
+  for t in test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done
   env
   LOUD=true ./runtests.sh
   sh -c "! grep '<failure>' results.xml"