diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-18 02:24:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-07-26 20:43:15 +0200 |
| commit | e3faeb71580f85394042028499bbc9573efc23cb (patch) | |
| tree | 266fcba2782bda74910aacb5714979bdc68a2bec /ide/preferences.mli | |
| parent | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (diff) | |
Adding a flag in CoqIDE to configure UNIX/Windows line ending.
Fixes both bugs #4924 and #4437.
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 426b0a328..801869d1d 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -11,6 +11,7 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] type tag = { tag_fg_color : string option; @@ -79,6 +80,7 @@ val window_height : int preference val auto_complete : bool preference val stop_before : bool preference val reset_on_tab_switch : bool preference +val line_ending : line_ending preference val vertical_tabs : bool preference val opposite_tabs : bool preference val background_color : string preference |