summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/scripts/parseargs.sh
diff options
context:
space:
mode:
Diffstat (limited to 'tools/memory-model/scripts/parseargs.sh')
-rw-r--r--tools/memory-model/scripts/parseargs.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 859e1d581e05..40f52080fdbd 100644
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -91,7 +91,7 @@ do
shift
;;
--herdopts|--herdopt)
- checkarg --destdir "(herd options)" "$#" "$2" '.*' '^--'
+ checkarg --destdir "(herd7 options)" "$#" "$2" '.*' '^--'
LKMM_HERD_OPTIONS="$2"
shift
;;