From 6b4965375402ac23392d2d451699c87005b4cbe8 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 22 May 2022 22:43:48 +0200 Subject: [PATCH] use in_character This addresses one aspect of #1472. --- src/lib/builtins.pl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/builtins.pl b/src/lib/builtins.pl index 3ddd056e..f4fa5104 100644 --- a/src/lib/builtins.pl +++ b/src/lib/builtins.pl @@ -1366,12 +1366,12 @@ char_code(Char, Code) :- ). get_char(C) :- - error:can_be(character, C), + error:can_be(in_character, C), current_input(S), '$get_char'(S, C). get_char(S, C) :- - error:can_be(character, C), + error:can_be(in_character, C), '$get_char'(S, C). can_be_number(N, PI) :- -- 2.54.0