[devel] Improved the options.awk script; added an "everything off" option.

This commit is contained in:
Glenn Randers-Pehrson
2010-04-28 07:52:16 -05:00
parent 34713ce23c
commit cd74549840
20 changed files with 247 additions and 79 deletions

View File

@@ -1,4 +1,4 @@
#!/bin/awk
#!/bin/awk -f
# Check a list of symbols against the master definition
# (official) list. Arguments:
#