From 18d61b8fe9cda8874a3f57b70a293492460ae574 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 12 Feb 2008 12:08:39 +0000 Subject: [PATCH] better error message in case inclusion failed --- helm/software/matita/matitaScript.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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)) ;; -- 2.39.2