Whitespacing.
commit097b686384cabbff672bb7fa72aa40fd8cd34211
authorGuillaume Yziquel <guillaume.hj.yziquel@gmail.com>
dateMon 17 Dec 2018, 13:31 (8 years ago)
parenta854dd6
jsrts/Runtime-javascript.js+2
@@ -7,7 +7,9 @@ $JSRTS.prim_systemInfo = function (index) {
77 }
88 return "";
99};
10+
1011$JSRTS.prim_writeStr = function (x) { return console.log(x) };
12+
1113$JSRTS.prim_readStr = function () { return prompt('Prelude.getLine') };
1214
1315$JSRTS.die = function (message) { throw new Error(message) };
jsrts/Runtime-node.js+4
@@ -1,5 +1,7 @@
11$JSRTS.os = require('os');
2+
23$JSRTS.fs = require('fs');
4+
35$JSRTS.prim_systemInfo = function (index) {
46 switch (index) {
57 case 0:
@@ -9,7 +11,9 @@ $JSRTS.prim_systemInfo = function (index) {
911 }
1012 return "";
1113};
14+
1215$JSRTS.prim_writeStr = function (x) { return process.stdout.write(x) };
16+
1317$JSRTS.prim_readStr = function () {
1418 var ret = '';
1519 var b = new Buffer(1024);