From 65cba90ea0baf38317d2d37eac16f0cafd9de241 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sun, 24 Jun 2018 09:06:34 +0200
Subject: [PATCH] Do not skip directories in case of typo.

---
 bench/bench                 | 6 ++++++
 bench/typing/x-good/.keepme | 0
 2 files changed, 6 insertions(+)
 create mode 100644 bench/typing/x-good/.keepme

diff --git a/bench/bench b/bench/bench
index 503fdc7d5..5eb08a0d0 100755
--- a/bench/bench
+++ b/bench/bench
@@ -15,6 +15,7 @@ suffix=$1
 goods () {
     pgm="bin/why3prove$suffix"
     ERROR=
+    test -d $1 || exit 1
     rm -f bench_errors
     for f in $1/*.[wm][hl][yw] ; do
 	printf "  $f... "
@@ -45,6 +46,7 @@ goods () {
 
 bads () {
     pgm="bin/why3prove$suffix"
+    test -d $1 || exit 1
     for f in $1/*.[wm][hl][yw] ; do
 	printf "  $f... "
 	if $pgm $2 $f > /dev/null 2>&1; then
@@ -59,6 +61,7 @@ bads () {
 
 drivers () {
     pgm="bin/why3prove$suffix"
+    test -d $1 || exit 1
     for f in $1/*.drv; do
         if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
         if [[ $f == drivers/c.drv ]]; then continue; fi
@@ -76,6 +79,7 @@ drivers () {
 
 valid_goals () {
     pgm="bin/why3prove$suffix"
+    test -d $1 || exit 1
     for f in $1/*.mlw; do
 	printf "  $f... "
         if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
@@ -90,6 +94,7 @@ valid_goals () {
 
 invalid_goals () {
     pgm="bin/why3prove$suffix"
+    test -d $1 || exit 1
     for f in $1/*.mlw; do
 	printf "  $f... "
 	if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
@@ -105,6 +110,7 @@ invalid_goals () {
 
 replay () {
     pgm="bin/why3replay$suffix"
+    test -d $1 || exit 1
     for f in $1/*/; do
         printf "  $f... "
         if $pgm $2 $f > /dev/null 2> /dev/null; then
diff --git a/bench/typing/x-good/.keepme b/bench/typing/x-good/.keepme
new file mode 100644
index 000000000..e69de29bb
-- 
GitLab