# HG changeset patch
# User wenzelm
# Date 1007485211 -3600
# Node ID b7ca1819866914c2a6ba8b4d71e3796a5c5b2794
# Parent  9c156045c8f2408c3f277adf981b36a21d428e7c
made slightly more robust;

diff -r 9c156045c8f2 -r b7ca18198669 doc-src/System/showsymbols
--- a/doc-src/System/showsymbols	Tue Dec 04 17:59:36 2001 +0100
+++ b/doc-src/System/showsymbols	Tue Dec 04 18:00:11 2001 +0100
@@ -20,4 +20,9 @@
     }
 }
 
+if ("$eol" eq "\\\\") {
+    print "$eol\n";
+}
+
 print "\\end{supertabular}\n";
+