diff options
Diffstat (limited to 'bin/info2head.fmt')
| -rw-r--r-- | bin/info2head.fmt | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/bin/info2head.fmt b/bin/info2head.fmt deleted file mode 100644 index 87eb1c8b1d0..00000000000 --- a/bin/info2head.fmt +++ /dev/null @@ -1,23 +0,0 @@ -start -hide section FILENAME -hide section COPYRIGHT -hide prelude -hide title -print synopsis -hide section CLASS TYPE -hide section AUDIENCE -hide section DESCRIPTION -hide section EXAMPLE -hide contract * -hide section * -hide section NOTES -hide section PORTABILITY -hide section SEE ALSO -hide section LIBRARY -hide section VERSION -hide section DATE RELEASED -hide section RCSID -hide section SCCSID -hide section AUTHOR(S) -hide copyright -end |