Never commit before trying to compile... stupid typo fixed.

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 5faab078fa48258fd883139e8edc65460d98f9c9..6bc725033352adce644a4d96558785ec195c7a9a 100644 (file)
--- 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 ();