diff --git a/etc/gaplint.sh b/etc/gaplint.sh index 57c8b27e6..a478f4697 100755 --- a/etc/gaplint.sh +++ b/etc/gaplint.sh @@ -1,4 +1,4 @@ #!/bin/bash set -e -gaplint --disable W004 *.g gap/* doc/*.xml tst/testinstall.tst tst/standard/*.tst tst/extreme/*.tst tst/workspaces/*.tst +gaplint --disable W004 $@ *.g gap/* doc/*.xml tst/testinstall.tst tst/standard/*.tst tst/extreme/*.tst tst/workspaces/*.tst