diff options
| -rw-r--r-- | coq/coqtags | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/coq/coqtags b/coq/coqtags index 21cd0bfa..a166a5a9 100644 --- a/coq/coqtags +++ b/coq/coqtags @@ -2,7 +2,6 @@ # # $Id$ # - undef $/; if($#ARGV<$[) {die "No Files\n";} |