diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 10f1ea827..0c5b7f6e1 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -80,6 +80,8 @@ type pref = mutable tab_length : int; mutable highlight_current_line : bool; + mutable nanoPG : bool; + } val save_pref : unit -> unit |