From f43d96aec71449e3b75e9fd732e87694cec5db8f Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 21 Mar 2013 14:22:36 +0000
Subject: Removing mandatory suffixes for library files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/check.ml b/checker/check.ml
index 88306e2148..03a18280a9 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -264,7 +264,7 @@ let try_locate_qualified_library qid =
 (*s Loading from disk to cache (preparation phase) *)
 
 let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
+  snd (System.raw_extern_intern Coq_config.vo_magic_number)
 
 let with_magic_number_check f a =
   try f a
-- 
cgit v1.2.3