Options declared but not parsed.

diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors
index ae1b592d0e8d491315182ca02701467b06a3b865..2ff61fe3673c3226a46444b5cf114dda93a21ed3 100755 (executable)
--- a/helm/software/matita/bench_disamberrors
+++ b/helm/software/matita/bench_disamberrors
@@ -9,6 +9,7 @@ while true ; do
   case "$1" in
     -d) libdir="$2"; shift 2 ;;
     -c) matitac="$2"; shift 2 ;;
+    -m) devel="$2"; shift 2 ;;
     --) shift; break ;;
      *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
   esac