diff options
Diffstat (limited to 'bin/info2head.fmt')
| -rw-r--r-- | bin/info2head.fmt | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/bin/info2head.fmt b/bin/info2head.fmt new file mode 100644 index 00000000000..87eb1c8b1d0 --- /dev/null +++ b/bin/info2head.fmt @@ -0,0 +1,23 @@ +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 |