Fix #1326: non-ascii character in print.js

josdejong · Nov 20, 2018 · 6baf6f0 · 6baf6f0
1 parent d09a7ff
commit 6baf6f0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/HISTORY.md b/HISTORY.md
@@ -3,6 +3,7 @@
 # not yet released, version 5.3.0
 
 - Implemented function `hasNumericValue`. Thanks @Sathish-kumar-Subramani.
+- Fix #1326: non-ascii character in print.js.
 
 
 # 2018-10-30, version 5.2.3

diff --git a/src/function/string/print.js b/src/function/string/print.js
@@ -51,7 +51,7 @@ function factory (type, config, load, typed) {
   const print = typed('print', {
     // note: Matrix will be converted automatically to an Array
     'string, Object | Array': _print,
-    'string, Object | Array, number | Object': _print
+    'string, Object | Array, number | Object': _print
   })
 
   print.toTex = undefined // use default template