changeset 10506 | 01333dbe1431 |
parent 10071 | ff08faf26d58 |
child 10639 | f902346264e9 |
--- 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;