summaryrefslogtreecommitdiff
path: root/library/goptions.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /library/goptions.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'library/goptions.ml')
-rw-r--r--library/goptions.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index c220544c..4d36e1c5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: goptions.ml 6304 2004-11-16 15:49:08Z sacerdot $ *)
+(* $Id: goptions.ml 9060 2006-07-27 15:30:35Z notin $ *)
(* This module manages customization parameters at the vernacular level *)
@@ -253,7 +253,7 @@ let declare_option cast uncast
unfreeze_function = write;
init_function = (fun () -> write default);
survive_module = false;
- survive_section = true}
+ survive_section = false}
in
fun v -> add_anonymous_leaf (decl_obj v)
else write