diff options
Diffstat (limited to 'coq/coqtags')
-rw-r--r-- | coq/coqtags | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/coq/coqtags b/coq/coqtags index b6c72c78..b51066ed 100644 --- a/coq/coqtags +++ b/coq/coqtags @@ -1,4 +1,7 @@ #!/usr/local/bin/perl4 +# +# $Id$ +# $/=0777; if($#ARGV<$[) {die "No Files\n";} |