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