From d551f35d2ff1f10c172540ccec5b6cd0e5aaf75d Mon Sep 17 00:00:00 2001 From: Jocelyn Fiat Date: Wed, 19 Jun 2024 08:36:35 +0200 Subject: [PATCH] added postcondition --- jj_vision/interface/views/view.e | 3 +++ 1 file changed, 3 insertions(+) diff --git a/jj_vision/interface/views/view.e b/jj_vision/interface/views/view.e index caa5978..b2789f0 100644 --- a/jj_vision/interface/views/view.e +++ b/jj_vision/interface/views/view.e @@ -59,6 +59,8 @@ feature {NONE} -- Initialization default_create set_target (a_target) -- calls `draw' -- draw + ensure + target_imp /= Void end create_interface_objects @@ -252,6 +254,7 @@ feature -- Element change draw ensure has_target: has_target (a_target) + target_imp /= Void end set_parent_view (a_view: VIEW)