diff options
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/buildtests.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/buildtests.sh b/scripts/buildtests.sh index d682f367..5b062505 100755 --- a/scripts/buildtests.sh +++ b/scripts/buildtests.sh @@ -373,6 +373,7 @@ SPLINT() { splint $files \ -badflag \ + -preproc \ -weak -warnposix \ -modobserver -initallelements -redef \ -linelen 1000 \ |