src/Tools/8bit/man/man1/gen-isa2latex.1
changeset 1826 2a2c0dbeb4ac
equal deleted inserted replaced
1825:88d4c33d7947 1826:2a2c0dbeb4ac
       
     1 .TH GEN-ISA2LATEX 1 "March 30, 1995"
       
     2 .AT 3
       
     3 .SH NAME
       
     4 gen-isa2latex \- a perl 4.x script
       
     5 .SH SYNOPSIS
       
     6 .B gen-isa2latex [options] tablefile 
       
     7 .SH DESCRIPTION
       
     8 .I gen-isa2latex
       
     9 generates an new converter for the Isabelle 8bit font. 
       
    10 See the file \fIconv-table.inp\fP in the directory
       
    11 \fIconfig\fP of the 8bit package for an example of a table file. It contains a
       
    12 lot of comments and is self explanatory.
       
    13 
       
    14 Options must be seperated by blanks.
       
    15 .SH OPTIONS
       
    16 .TP 5
       
    17 .B \-d "\t"
       
    18 turn on debug mode. The script will tell you what it is doing.
       
    19 
       
    20 .TP 5
       
    21 .B \-dd "\t"
       
    22 turn on deep debug mode. This is very verbose.
       
    23 
       
    24 .SH ENVIRONMENT
       
    25 No environment variables are used.
       
    26 .SH FILES
       
    27 None.
       
    28 .SH AUTHOR
       
    29 Franz Regensburger
       
    30 .SH "SEE ALSO"
       
    31 
       
    32 .SH DIAGNOSTICS
       
    33 
       
    34 .SH BUGS
       
    35