From 1992749e785762338f83f03fc38717757daab98e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jan 2018 18:52:00 -0800 Subject: [PATCH] to ascii or not to ascii #1447 Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 45ea9be23..18878d6ea 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1696,7 +1696,11 @@ if _lib is None: def _to_ascii(s): if isinstance(s, str): - return s.encode('ascii') + try: + return s.encode('ascii') + except: + # kick the bucket down the road. :-J + return s else: return s