changeset 9961 | 5a9626118941 |
parent 9789 | 7e5e6c47c0b5 |
--- a/lib/scripts/symbolinput.pl Fri Sep 15 00:16:08 2000 +0200 +++ b/lib/scripts/symbolinput.pl Fri Sep 15 00:16:36 2000 +0200 @@ -84,7 +84,7 @@ "\xe9", "\\<Leftarrow>", "\xea", "\\<Midarrow>", "\xeb", "\\<Rightarrow>", - "\xec", "\\<bow>", + "\xec", "\\<frown>", "\xed", "\\<mapsto>", "\xee", "\\<leadsto>", "\xef", "\\<up>",