diff options
| -rwxr-xr-x | scripts/gen_gki_modules_headers.sh | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/scripts/gen_gki_modules_headers.sh b/scripts/gen_gki_modules_headers.sh index ad0eeee28565..9fab5185db19 100755 --- a/scripts/gen_gki_modules_headers.sh +++ b/scripts/gen_gki_modules_headers.sh @@ -26,12 +26,6 @@ set -e # # Common Definitions # -# Use "make V=1" to debug this script. -case "$KBUILD_VERBOSE" in -*1*) - set -x - ;; -esac # # generate_header(): @@ -44,6 +38,7 @@ generate_header() { local symbol_file=$2 local symbol_type=$3 + echo " GEN ${header_file}" if [ -f "${header_file}" ]; then rm -f -- "${header_file}" fi |