diff options
| author | Dmitry Torokhov <[email protected]> | 2019-09-16 09:56:27 -0700 |
|---|---|---|
| committer | Dmitry Torokhov <[email protected]> | 2019-09-16 09:56:27 -0700 |
| commit | 0898782247ae533d1f4e47a06bc5d4870931b284 (patch) | |
| tree | 21f75cc590542a870f42350b9410fc0588f02b79 /tools/memory-model/scripts/parseargs.sh | |
| parent | 0c043d70d04711fe6c380df9065fdc44192c49bf (diff) | |
| parent | 410f25de467ee94c1a577c6ee7370c37b376c17c (diff) | |
Merge branch 'next' into for-linus
Prepare input updates for 5.4 merge window.
Diffstat (limited to 'tools/memory-model/scripts/parseargs.sh')
| -rw-r--r-- | tools/memory-model/scripts/parseargs.sh | 2 |
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 ;; |