version 1.5, 2002/07/25 15:19:03
|
version 1.6, 2002/07/30 18:24:44
|
Line 34 if ( scalar(@ARGV) < 2 )
|
Line 34 if ( scalar(@ARGV) < 2 )
|
print (<<USAGE); |
print (<<USAGE); |
Usage: $0 texxml_file_name or |
Usage: $0 texxml_file_name or |
perl $0 -- texxml_file_name |
perl $0 -- texxml_file_name |
where "texxml_file_name" does not include the .texxml suffix |
where "texxml_file_name" optionally includes the extension |
Output: texxml_file_name.dvi |
Output: texxml_file_name.dvi |
|
|
$0 renders texxml files into dvi files by copying the tex file |
$0 renders texxml files into dvi files by copying the tex file |
Line 53 USAGE
|
Line 53 USAGE
|
|
|
my $tmpdir = tmpnam(); |
my $tmpdir = tmpnam(); |
my $fileroot = $ARGV[1]; |
my $fileroot = $ARGV[1]; |
|
|
|
if (substr($fileroot, -7) eq ".texxml") |
|
{ |
|
$fileroot = substr($fileroot, 0, -7); |
|
} |
|
|
my $epssource = "/home/httpd/html/adm/help/eps"; |
my $epssource = "/home/httpd/html/adm/help/eps"; |
|
|
if ( defined ( $ARGV[2] ) ) # override eps source, for build on install |
if ( defined ( $ARGV[2] ) ) # override eps source, for build on install |