etc/options
changeset 52779 82707f95a783
parent 52773 3e8b9d2f18cb
child 52798 9d3c9862d1dd
equal deleted inserted replaced
52778:19fa3e3964f0 52779:82707f95a783
   125 
   125 
   126 option editor_execution_priority : int = -1
   126 option editor_execution_priority : int = -1
   127   -- "execution priority of main document structure (e.g. 0, -1, -2)"
   127   -- "execution priority of main document structure (e.g. 0, -1, -2)"
   128 
   128 
   129 option editor_execution_range : string = "visible"
   129 option editor_execution_range : string = "visible"
   130   -- "range of continuous document processing: all, none, visible"
   130   -- "execution range of continuous document processing: all, none, visible"
   131 
   131 
   132 
   132 
   133 section "Miscellaneous Tools"
   133 section "Miscellaneous Tools"
   134 
   134 
   135 public option find_theorems_limit : int = 40
   135 public option find_theorems_limit : int = 40