From e3faeb71580f85394042028499bbc9573efc23cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 Jul 2016 02:24:42 +0200 Subject: Adding a flag in CoqIDE to configure UNIX/Windows line ending. Fixes both bugs #4924 and #4437. --- ide/preferences.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'ide/preferences.mli') 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 -- cgit v1.2.3