diff --git a/dev/check-files.sh b/dev/check-files.sh index 7a77ad646ea937a6bf898ab417dadd8d7911a16c..b442ae45ad40451440a671be11ec26d47cf7ee1f 100755 --- a/dev/check-files.sh +++ b/dev/check-files.sh @@ -73,7 +73,8 @@ if [ "$MODE" = "all" ]; then make $LINT || exit 1 fi if [ $DO_HDRCK = "yes" ] ; then - make $HDRCK HDRCK_EXTRA="-quiet" || exit 1 + # Don't define HDRCK_EXTRA, that is required by external plugins + make $HDRCK || exit 1 fi else STAGED=$(git diff --diff-filter ACMR --name-only --cached $REFERENCE | sort) @@ -105,16 +106,17 @@ else TMP=$(mktemp) cleanup () { - rm "$TMP" + rm -f "$TMP" } trap cleanup exit - git check-attr -za $STAGED > "$TMP" if [ $DO_LINT = "yes" ] ; then + git check-attr -za $STAGED > "$TMP" make $LINT LINTCK_FILES_INPUT="$TMP" || exit 1 fi - git check-attr -z header_spec $STAGED > "$TMP" if [ $DO_HDRCK = "yes" ] ; then - make $HDRCK HDRCK_FILES_INPUT="$TMP" HDRCK_EXTRA="-quiet" || exit 1 + git check-attr -z header_spec $STAGED > "$TMP" + # Don't define HDRCK_EXTRA, that is required by external plugins + make $HDRCK HDRCK_FILES_INPUT="$TMP" || exit 1 fi fi diff --git a/tools/hdrck/hdrck.ml b/tools/hdrck/hdrck.ml index 339ef47453951e69d545811ef186762de2f3e449..409c06b32eae15abcc0a3a12f0c83cc9ac908841 100644 --- a/tools/hdrck/hdrck.ml +++ b/tools/hdrck/hdrck.ml @@ -60,7 +60,7 @@ and headache_config_file = ref [] (* empty -> headache_config_file_default *) and headache_config_file_default = "headers/headache_config.txt" and exit_on_warning = ref false and exit_on_error = ref true (* only settable to false for debugging purposes *) -and quiet = ref false +and quiet = ref true type mode = | Check @@ -632,6 +632,8 @@ let rec argspec = [ " enable debug messages"; "-quiet", Arg.Set quiet, "disable most messages"; + "-verbose", Arg.Unit (fun () -> quiet := false), + "print some informative messages"; "-forbidden-headers", Arg.String (fun set -> set_cumulative ~name:"-forbidden-headers" forbidden_headers ~set) , "<license name>,... \t none of the checked files may have one of the <license name> []";