--- doc/help/render.texxml.pl	2002/07/19 17:00:05	1.4
+++ doc/help/render.texxml.pl	2002/07/30 18:24:44	1.6
@@ -34,7 +34,7 @@ if ( scalar(@ARGV) < 2 )
     print (<<USAGE);
 Usage: $0 texxml_file_name or
        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
 
 $0 renders texxml files into dvi files by copying the tex file
@@ -53,6 +53,12 @@ USAGE
 
 my $tmpdir = tmpnam();
 my $fileroot = $ARGV[1];
+
+if (substr($fileroot, -7) eq ".texxml")
+{
+    $fileroot = substr($fileroot, 0, -7);
+}
+
 my $epssource = "/home/httpd/html/adm/help/eps";
 
 if ( defined ( $ARGV[2] ) ) # override eps source, for build on install
@@ -62,7 +68,7 @@ if ( defined ( $ARGV[2] ) ) # override e
 
 my $redir = ">& /dev/null"; # empty this for easier debugging
 
-mkdir $tmpdir;
+mkdir $tmpdir, 0755;
 
 print "Converting texxml to tex...\n";
 system ( "perl texxml2latex.pl $fileroot.texxml > $tmpdir/$fileroot.tex" );