From f09a7177199788e83194fc261eb7a5584d03371b Mon Sep 17 00:00:00 2001
From: jmoenig <jens@moenig.org>
Date: Fri, 18 Jul 2014 15:36:56 +0200
Subject: rename "character" to "letter" in delimiter list
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

of “split” block
---
 threads.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'threads.js')

diff --git a/threads.js b/threads.js
index 24d4196..469fb7f 100644
--- a/threads.js
+++ b/threads.js
@@ -83,7 +83,7 @@ ArgLabelMorph, localize, XML_Element, hex_sha512*/
 
 // Global stuff ////////////////////////////////////////////////////////
 
-modules.threads = '2014-July-11';
+modules.threads = '2014-July-18';
 
 var ThreadManager;
 var Process;
@@ -2148,7 +2148,7 @@ Process.prototype.reportTextSplit = function (string, delimiter) {
         break;
     case 'whitespace':
         return new List(str.trim().split(/[\t\r\n ]+/));
-    case 'character':
+    case 'letter':
         del = '';
         break;
     default:
-- 
cgit v1.3.1