fix reporting state of unknown flag (obs from Paulo Moura).
This commit is contained in:
parent
0cd9009132
commit
7d37428f36
@ -372,8 +372,8 @@ unknown(V0,V) :-
|
|||||||
|
|
||||||
|
|
||||||
'$ask_unknown_flag'(Old) :-
|
'$ask_unknown_flag'(Old) :-
|
||||||
recorded('$unknown','$unkonwn'(_,MyOld),_), !,
|
recorded('$unknown','$unknown'(_,MyOld),_), !,
|
||||||
'$cleanup_unknwon_handler'(MyOld,Old).
|
'$cleanup_unknown_handler'(MyOld,Old).
|
||||||
'$ask_unknown_flag'(fail).
|
'$ask_unknown_flag'(fail).
|
||||||
|
|
||||||
'$cleanup_unknown_handler'('$unknown_error'(_),error) :- !.
|
'$cleanup_unknown_handler'('$unknown_error'(_),error) :- !.
|
||||||
|
Reference in New Issue
Block a user