src/Tools/jEdit/etc/options
changeset 60973 d94f3afd69b6
parent 60916 a6e2a667b0a8
child 61011 018b0c996b54
equal deleted inserted replaced
60972:4fc468197040 60973:d94f3afd69b6
     7   -- "default print modes for output, separated by commas (change requires restart)"
     7   -- "default print modes for output, separated by commas (change requires restart)"
     8 
     8 
     9 public option jedit_auto_load : bool = false
     9 public option jedit_auto_load : bool = false
    10   -- "load all required files automatically to resolve theory imports"
    10   -- "load all required files automatically to resolve theory imports"
    11 
    11 
    12 public option jedit_auto_resolve : bool = true
    12 public option jedit_auto_resolve : bool = false
    13   -- "automatically resolve auxiliary files within the editor"
    13   -- "automatically resolve auxiliary files within the editor"
    14 
    14 
    15 public option jedit_reset_font_size : int = 18
    15 public option jedit_reset_font_size : int = 18
    16   -- "reset main text font size"
    16   -- "reset main text font size"
    17 
    17