equal
deleted
inserted
replaced
1 #!/usr/local/dist/bin/perl |
|
2 'di'; |
|
3 'ig00'; |
|
4 # |
|
5 # $Header$ |
|
6 # |
|
7 # $Log$ |
|
8 # Revision 1.3 1998/10/19 13:37:02 oheimb |
|
9 # corrected Header |
|
10 # |
|
11 # Revision 1.2 1997/03/17 11:25:52 wenzelm |
|
12 # fixed perl path; |
|
13 # |
|
14 # Revision 1.1.1.1 1996/06/25 15:44:59 oheimb |
|
15 # Graphical 8bit Font Packet, see isabelle/Tools/8bit/doc/manual.dvi |
|
16 # Author: Franz Regensburger; improvements by David von Oheimb |
|
17 # |
|
18 # Revision 1.1.1.1 1996/06/25 13:58:23 oheimb |
|
19 # Graphical 8bit Font Package imported, second attempt |
|
20 # |
|
21 # |
|
22 # isapal.pl |
|
23 # Franz Regensburger <regensbu@informatik.tu-muenchen.de> |
|
24 # 21.3.95 |
|
25 # |
|
26 # last changed: |
|
27 # |
|
28 # print the file palette.isa |
|
29 # |
|
30 # needs an 8bit terminal for output |
|
31 |
|
32 $pack=$ENV{'ISABELLE8BIT'}; |
|
33 $filename = "$pack/doc/palette.isa"; |
|
34 |
|
35 open(INFILE,$filename) || die "can't open $filename: $!\n"; |
|
36 |
|
37 while (<INFILE>){ print;} |
|
38 |
|
39 close(INFILE); |
|
40 exit(0); |
|
41 |
|
42 ############################################################### |
|
43 |
|
44 # These next few lines are legal in both Perl and nroff. |
|
45 |
|
46 .00; # finish .ig |
|
47 |
|
48 'di \" finish diversion--previous line must be blank |
|
49 .nr nl 0-1 \" fake up transition to first page again |
|
50 .nr % 0 \" start at page 1 |
|
51 '; __END__ ##### From here on it's a standard manual page ##### |
|