etc/symbols
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
-