src/Tools/jEdit/etc/options
changeset 61023 46df28442a80
parent 61011 018b0c996b54
child 61139 f9fd43d8981d
equal deleted inserted replaced
61022:1c4ae64636bb 61023:46df28442a80
     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 = false
    12 public option jedit_auto_resolve : bool = true
    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