From dfc88cb4e7d0dca81cabe418d2c732cd22166726 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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