From dfc88cb4e7d0dca81cabe418d2c732cd22166726 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 17:07:07 +0000
Subject: [PATCH] Never commit before trying to compile... stupid typo fixed.
---
helm/software/components/ng_kernel/check.ml | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 5faab078f..6bc725033 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -127,11 +127,10 @@ let _ =
NCicTypeChecker.typecheck_obj o
with
| NCicTypeChecker.AssertFailure s
- | NCicTypeChecker.TypeCheckerFailure s as e ->
+ | NCicTypeChecker.TypeCheckerFailure s
+ | NCicEnvironment.ObjectNotFound s as e ->
prerr_endline ("######### " ^ Lazy.force s);
if not ignore_exc then raise e
- | NCicEnvironment.Object_not_found s ->
- prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)
)
alluris;
NCicEnvironment.invalidate ();
--
2.39.2