From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Nov 2010 20:25:00 +0000 (+0000)
Subject: - bug fixed: fullpath used in place of relative path
X-Git-Tag: make_still_working~2706
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c881200303035c81106f09c4fafb06119a38c157;p=helm.git

- bug fixed: fullpath used in place of relative path
---

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 1efaeff24..cd5c83441 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -288,7 +288,7 @@ and compile ~compiling ~include_paths fname =
 (* BIG BUG: if a file recursively includes itself, anything can happen,
  * from divergence to inclusion of an old copy of itself *)
 and assert_ng ~compiling ~include_paths ~root mapath =
- let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
+ let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  assert (root=root');
  let baseuri = NUri.uri_of_string baseuri in
  let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
@@ -297,8 +297,8 @@ and assert_ng ~compiling ~include_paths ~root mapath =
    Some (Unix.stat ngpath).Unix.st_mtime
   with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
  let matime =
-  try (Unix.stat mapath).Unix.st_mtime
-  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false
+  try (Unix.stat fullmapath).Unix.st_mtime
+  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
  in
  let to_be_compiled =
   match ngtime with
@@ -317,7 +317,7 @@ and assert_ng ~compiling ~include_paths ~root mapath =
      (* maybe recompiling it I would get the same... *)
      raise (AlreadyLoaded (lazy mapath))
    else
-    (compile ~compiling ~include_paths mapath; true)
+    (compile ~compiling ~include_paths fullmapath; true)
 ;;
 
 let assert_ng = assert_ng ~compiling:[]