--- doc/help/render.texxml.pl	2002/08/09 14:48:31	1.7
+++ doc/help/render.texxml.pl	2002/08/12 16:20:40	1.8
@@ -59,6 +59,12 @@ if (substr($fileroot, -7) eq ".texxml")
     $fileroot = substr($fileroot, 0, -7);
 }
 
+if ( -e "$fileroot.pdf" )
+{
+    print "$fileroot already built.\n";
+    exit();
+}
+
 my $epssource = "/home/httpd/html/adm/help/eps";
 
 if ( defined ( $ARGV[2] ) ) # override eps source, for build on install