# HG changeset patch
# User wenzelm
# Date 974829807 -3600
# Node ID 01333dbe1431bc05169853d880d56f15af1dce3f
# Parent  b89e6cc963e3d43576be786c5eeee4f9cebdbec7
replace \<dots>;

diff -r b89e6cc963e3 -r 01333dbe1431 lib/scripts/unsymbolize.pl
--- a/lib/scripts/unsymbolize.pl	Tue Nov 21 19:03:06 2000 +0100
+++ b/lib/scripts/unsymbolize.pl	Tue Nov 21 19:03:27 2000 +0100
@@ -22,6 +22,7 @@
     s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
     s/\\?\\<Rightarrow>/=>/g;
     s/\\?\\<equiv>/==/g;
+    s/\\?\\<dots>/.../g;
     s/\\?\\<lbrakk> ?/[| /g;
     s/\\?\\ ?<rbrakk>/ |]/g;
     s/\\?\\<lparr> ?/(| /g;