Merge fc4927be5b into 757bfefc6d

2025-04-20 08:43:40 +02:00 · 2017-01-16 15:43:47 +00:00 · 2017-01-16 15:43:47 +00:00 · cdfaddc02d
commit cdfaddc02d
parent 757bfefc6d fc4927be5b
1 changed files with 5 additions and 5 deletions
--- a/10
+++ b/10
@ -1991,11 +1991,11 @@ do
            shift
            break
            ;;
-        # -*)
-        #     UNKNOWNOPTIONS=$((UNKNOWNOPTIONS+$1))
-        #     # echo "WARN: Unknown option (ignored): $1" >&2
-        #     shift
-        #     ;;
+        -*)
+            UNKNOWNOPTIONS=$((UNKNOWNOPTIONS+$1))
+            echo "$0: Unknown option: $1" >&2
+            exit 1
+            ;;
        *)  # no more options we understand.
            break
            ;;