From 774a61b47ec0d3c312fad8d47d0e72f929f5cb7e Mon Sep 17 00:00:00 2001
From: Orestis Floros <orestisf1993@gmail.com>
Date: Wed, 14 Mar 2018 14:59:26 +0200
Subject: [PATCH] dump-asy.pl: Add marks
---
contrib/dump-asy.pl | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/contrib/dump-asy.pl b/contrib/dump-asy.pl
index 9bb2db3a..636b20ce 100755
--- a/contrib/dump-asy.pl
+++ b/contrib/dump-asy.pl
@@ -47,7 +47,8 @@ sub dump_node {
if (!defined($n->{window})) {
$type = $n->{layout};
}
- my $name = qq|``$na'' ($type)|;
+ my $marks = $n->{marks} ? ' [' . join('][', @{$n->{marks}}) . ']' : '';
+ my $name = qq|``$na'' ($type)$marks|;
print $tmp "TreeNode n" . $n->{id} . " = makeNode(";