ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

javascript: fix for #1580

Browse Source
This commit is contained in:
raichoo 2014-10-05 00:24:54 +02:00
parent 981b29f1ac
commit eb9eadd249
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
jsrts/Runtime-common.js
View File

@ -16,6 +16,14 @@ var i$valstack_base;
var i$ret;
var i$callstack;
var i$Int = {};
var i$String = {};
var i$Integer = {};
var i$Float = {};
var i$Char = {};
var i$Ptr = {};
var i$Forgot = {};
/** @constructor */
var i$CON = function(tag,args,app,ev) {
this.tag = tag;