Skip to content

Commit 2ba8dc1

Browse files
committed
Compiles with 0.10-git:36448f9 Idris.
1 parent d5664d4 commit 2ba8dc1

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

IdrisScript/Timer.idr

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ import IdrisScript
44

55
%access public
66

7-
abstract
7+
export
88
record Timeout where
99
constructor MkTimeout
1010
unTimeout : Ptr
1111

12-
abstract
12+
export
1313
record Interval where
1414
constructor MkInterval
1515
unInterval : Ptr
@@ -36,6 +36,7 @@ setInterval f millis = do
3636
return $ MkInterval interval
3737

3838
||| Clears an interval.
39+
export
3940
clearInterval : Interval -> JS_IO ()
4041
clearInterval interval =
4142
jscall "clearInterval(%0)" (Ptr -> JS_IO ()) (unInterval interval)

0 commit comments

Comments
 (0)