| changeset 69592 | a80d8ec6c998 |
| parent 69589 | e15f053a42d8 |
| child 69603 | 67ae2e164c0f |
--- a/etc/options Thu Jan 03 22:30:41 2019 +0100 +++ b/etc/options Fri Jan 04 21:49:06 2019 +0100 @@ -285,6 +285,9 @@ option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" +option update_control_cartouches : bool = false + -- "update antiquotations to use control symbol with cartouche argument" + section "Build Database"