From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 12 Feb 2008 12:08:39 +0000 (+0000)
Subject: better error message in case inclusion failed
X-Git-Tag: make_still_working~5619
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18d61b8fe9cda8874a3f57b70a293492460ae574;p=helm.git

better error message in case inclusion failed
---

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 828002a8b..477e775d8 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -140,7 +140,11 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
-      if b then f ~include_paths x 
+      if b then 
+        try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
+         raise 
+           (Failure ("Including: "^tgt^
+             "\nNothing to do... did you run matitadep?"))
       else raise (Failure ("Compiling: " ^ tgt))
 ;;