diff --git a/Benchmark_instances/dont_submit b/Benchmark_instances/dont_submit new file mode 100644 index 00000000000..b81babb87ff --- /dev/null +++ b/Benchmark_instances/dont_submit @@ -0,0 +1,4 @@ +description.txt +developer_scripts +maintainer +out_html