changeset 69586 | 9171d1ce5a35 |
parent 69572 | 09a6a7c04b45 |
child 69589 | e15f053a42d8 |
--- a/etc/options Thu Jan 03 21:04:16 2019 +0100 +++ b/etc/options Thu Jan 03 21:06:39 2019 +0100 @@ -277,6 +277,12 @@ option export_theory : bool = false +section "Theory update" + +option update_mixfix_cartouches : bool = false + -- "update mixfix templates to use cartouches instead of double quotes" + + section "Build Database" option build_database_server : bool = false