diff options
| -rwxr-xr-x | make-reg-dotc | 4 | ||||
| -rwxr-xr-x | make-tapreg-dotc | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/make-reg-dotc b/make-reg-dotc index 8aee132667..47cc31732a 100755 --- a/make-reg-dotc +++ b/make-reg-dotc @@ -1,6 +1,10 @@ #! /bin/sh # +# $Id: make-reg-dotc,v 1.8 2004/05/03 18:53:16 guy Exp $ +# + +# # The first argument is the output filename. # diff --git a/make-tapreg-dotc b/make-tapreg-dotc index d3c470529c..f2acb5994d 100755 --- a/make-tapreg-dotc +++ b/make-tapreg-dotc @@ -1,6 +1,10 @@ #! /bin/sh # +# $Id: make-tapreg-dotc,v 1.4 2004/05/03 18:53:57 guy Exp $ +# + +# # The first argument is the output filename. # |