call_cleanup/3 should allow exceptions to go through, even if cleaner
itself calls an exception (obs from Ulrich Neumerkel).
This commit is contained in:
parent
eef4b3cad2
commit
e3aeb48af6
@ -64,7 +64,8 @@ call_cleanup(Goal, Catcher, Cleanup) :-
|
||||
'$cleanup_exception'(Exception,Catcher,Cleanup)).
|
||||
|
||||
'$cleanup_exception'(Exception, exception(Exception), Cleanup) :- !,
|
||||
'$clean_call'(Cleanup),
|
||||
% whatever happens, let exception go through
|
||||
catch('$clean_call'(Cleanup),_,true),
|
||||
throw(Exception).
|
||||
'$cleanup_exception'(Exception, _, _) :-
|
||||
throw(Exception).
|
||||
|
Reference in New Issue
Block a user