changeset 74568 | 7f311d474cf9 |
parent 74433 | ec1774613824 |
child 74570 | 7625b5d7cfe2 |
--- a/etc/symbols Sun Oct 24 16:43:54 2021 +0200 +++ b/etc/symbols Sun Oct 24 18:02:58 2021 +0200 @@ -456,6 +456,7 @@ \<^cterm> argument: cartouche \<^ctyp> argument: cartouche \<^keyword> argument: cartouche +\<^let> argument: cartouche \<^locale> argument: cartouche \<^make_judgment> \<^dest_judgment> @@ -505,4 +506,3 @@ \<^if_macos> argument: cartouche \<^if_windows> argument: cartouche \<^if_unix> argument: cartouche -