diff options
-rwxr-xr-x | tools/ci/scripts/deheader.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/ci/scripts/deheader.sh b/tools/ci/scripts/deheader.sh index ddf60169d..0d7953b88 100755 --- a/tools/ci/scripts/deheader.sh +++ b/tools/ci/scripts/deheader.sh @@ -19,5 +19,6 @@ ${dir}/deheader -q -i "\"debug.h\"" \ -i "\"$name\"" \ -c "$CXX" \ -d "$FLAGS" \ --m "-c -std=gnu++1z -Werror -Wall -Wextra -Wundef -Wmissing-declarations -DLOCALEDIR=\\\"\\\" -I/usr/include $INCLUDES -I${dir}/src" $1 \ +-s "-std=gnu++1z" \ +-m "-c -Werror -Wall -Wextra -Wundef -Wmissing-declarations -DLOCALEDIR=\\\"\\\" -I/usr/include $INCLUDES -I${dir}/src" $1 \ | grep -v "portability requires" | tee -a ${LOGFILE} |