etc: pass command line args to gaplint in etc/gaplint.sh

digraphs · Jan 5, 2024 · 772a486 · 772a486
1 parent f496d06
commit 772a486
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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