lib/Tools/doc
changeset 2940 baae674b1d29
parent 2936 bd33e7aae062
child 3007 e5efa177ee0c
equal deleted inserted replaced
2939:73837efaf71b 2940:baae674b1d29
     1 #!/bin/bash -norc
     1 #!/bin/bash -norc
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: view Isabelle documentation
     5 # DESCRIPTION: view Isabelle documentation
     6 #
       
     7 # TODO:
       
     8 #  - other formats than dvi (??)
       
     9 
     6 
    10 
     7 
    11 PRG=$(basename $0)
     8 PRG=$(basename $0)
    12 
     9 
    13 function usage()
    10 function usage()