aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2006-07-13 10:14:40 +0000
committerherbelin2006-07-13 10:14:40 +0000
commitb10fc3d338314db1b3a4ee1097982cc8cf859e1b (patch)
tree98bb06382f214deca7a6d375f0c8ccfb79c2d88a
parentce0a9574ac47f333d5906cf627123d932ebf2c74 (diff)
Nombre magique pour la 8.1beta
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9048 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--library/library.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index c5082b307e..73d58b5499 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -300,7 +300,7 @@ let (in_import, out_import) =
(*s Loading from disk to cache (preparation phase) *)
-let vo_magic_number = 08003 (* V8.0 final new syntax + new params in ind *)
+let vo_magic_number = 08099 (* V8.1 beta *)
let (raw_extern_library, raw_intern_library) =
System.raw_extern_intern vo_magic_number ".vo"