make sure call_cleanup makes exception handler fail.
This commit is contained in:
parent
9ce8df7bcd
commit
848e1209a2
@ -65,8 +65,12 @@ call_cleanup(Goal, Catcher, Cleanup) :-
|
|||||||
|
|
||||||
'$cleanup_exception'(Exception, exception(Exception), Cleanup) :- !,
|
'$cleanup_exception'(Exception, exception(Exception), Cleanup) :- !,
|
||||||
% whatever happens, let exception go through
|
% whatever happens, let exception go through
|
||||||
catch('$clean_call'(Cleanup),_,true),
|
(
|
||||||
throw(Exception).
|
catch('$clean_call'(Cleanup),_,fail),
|
||||||
|
fail
|
||||||
|
;
|
||||||
|
throw(Exception)
|
||||||
|
).
|
||||||
'$cleanup_exception'(Exception, _, _) :-
|
'$cleanup_exception'(Exception, _, _) :-
|
||||||
throw(Exception).
|
throw(Exception).
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user