equal
deleted
inserted
replaced
1 #!/usr/local/dist/DIR/perl4/bin/perl |
1 #!/usr/local/dist/bin/perl |
2 'di'; |
2 'di'; |
3 'ig00'; |
3 'ig00'; |
4 # |
4 # |
5 # $Header$ |
5 # $Header$ |
6 # |
6 # |
7 # $Log$ |
7 # $Log$ |
8 # Revision 1.1 1996/06/25 15:44:59 oheimb |
8 # Revision 1.2 1997/03/17 11:25:52 wenzelm |
9 # Initial revision |
9 # fixed perl path; |
|
10 # |
|
11 # Revision 1.1.1.1 1996/06/25 15:44:59 oheimb |
|
12 # Graphical 8bit Font Packet, see isabelle/Tools/8bit/doc/manual.dvi |
|
13 # Author: Franz Regensburger; improvements by David von Oheimb |
10 # |
14 # |
11 # Revision 1.1.1.1 1996/06/25 13:58:23 oheimb |
15 # Revision 1.1.1.1 1996/06/25 13:58:23 oheimb |
12 # Graphical 8bit Font Package imported, second attempt |
16 # Graphical 8bit Font Package imported, second attempt |
13 # |
17 # |
14 # |
18 # |