aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorherbelin2008-03-04 19:59:14 +0000
committerherbelin2008-03-04 19:59:14 +0000
commitd99b9b0e1fe7f5614bd5b1423161c25705a72eea (patch)
tree8476115de84f8182f3bddc014a04a117ff457b26 /ide
parent0051fd0b4fdc72b3c13907f456c86d4b96f00695 (diff)
Branchement de l'auto-save de coqide par défaut
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10619 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/preferences.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d03afa3a99..91c2cc9fcc 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -110,7 +110,7 @@ let (current:pref ref) =
global_auto_revert = false;
global_auto_revert_delay = 10000;
- auto_save = false;
+ auto_save = true;
auto_save_delay = 10000;
auto_save_name = "#","#";