--- doc/help/render.texxml.pl	2002/07/25 15:19:03	1.5
+++ 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