contrib/dump-asy.pl: Display nicer double-quotes

The right way to do this in LaTeX is ``foo'', not "foo".

diff --git a/contrib/dump-asy.pl b/contrib/dump-asy.pl
index c75dfcd05cdc2bd047d63130c2202f7956ca60a9..3ebdb858e9ef275d830765b1a54a75639790b6c4 100755 (executable)
--- a/contrib/dump-asy.pl
+++ b/contrib/dump-asy.pl
@@ -40,7 +40,7 @@ sub dump_node {
     if (!defined($n->{window})) {
         $type = $n->{orientation} . '-split';
     }
-    my $name = qq|\\"$na\\" ($type)|;
+    my $name = qq|``$na'' ($type)|;
 
     print $tmp "TreeNode n" . $n->{id} . " = makeNode(";