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