src/Tools/8bit/man/man1/gen-isa2latex.1
changeset 1826 2a2c0dbeb4ac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/man/man1/gen-isa2latex.1	Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,35 @@
+.TH GEN-ISA2LATEX 1 "March 30, 1995"
+.AT 3
+.SH NAME
+gen-isa2latex \- a perl 4.x script
+.SH SYNOPSIS
+.B gen-isa2latex [options] tablefile 
+.SH DESCRIPTION
+.I gen-isa2latex
+generates an new converter for the Isabelle 8bit font. 
+See the file \fIconv-table.inp\fP in the directory
+\fIconfig\fP of the 8bit package for an example of a table file. It contains a
+lot of comments and is self explanatory.
+
+Options must be seperated by blanks.
+.SH OPTIONS
+.TP 5
+.B \-d "\t"
+turn on debug mode. The script will tell you what it is doing.
+
+.TP 5
+.B \-dd "\t"
+turn on deep debug mode. This is very verbose.
+
+.SH ENVIRONMENT
+No environment variables are used.
+.SH FILES
+None.
+.SH AUTHOR
+Franz Regensburger
+.SH "SEE ALSO"
+
+.SH DIAGNOSTICS
+
+.SH BUGS
+