| commit | d252f7a4061155abaa1c9817069eed8888c79543 | [log] [tgz] |
|---|---|---|
| author | Jonatan Antoni <jonatan.antoni@arm.com> | Thu May 12 17:47:34 2022 +0200 |
| committer | Jonatan Antoni <jonatan.antoni@arm.com> | Thu May 12 18:50:26 2022 +0200 |
| tree | e971726902ab5158a12dcbb31ac0c1acaf91e6c4 | |
| parent | f9d30ef0086687151a581189b524868d6b9c869b [diff] [blame] |
Enhance check_header.sh to consider all commits in a PR.
diff --git a/CMSIS/Utilities/fetch_devtools.sh b/CMSIS/Utilities/fetch_devtools.sh index f3c6699..2b7b09b 100755 --- a/CMSIS/Utilities/fetch_devtools.sh +++ b/CMSIS/Utilities/fetch_devtools.sh
@@ -42,7 +42,7 @@ exit 1 ;; '-f'|'--force') - FORCE=1 + FORCE=1 ;; *) # unknown option POSITIONAL+=("$1") # save it in an array for later