@@ -27,16 +27,6 @@ issue the following command:
2727 $ idris --codegen javascript hello.idr -o hello.js
2828
2929
30−Generating code for NodeJS is slightly different. Idris outputs a
31−JavaScript file that can be directly executed via node.
32−
33−::
34−
35− $ idris --codegen node hello.idr -o hello
36− $ ./hello
37− Hello world
38−
39−
4030Idris can produce very big chunks of JavaScript code (hello world
4131weighs in at 1500 lines). However, the generated code can be minified
4232using the `closure-compiler
@@ -50,6 +40,16 @@ using the `closure-compiler
5040Node.js
5141-------
5242
43+Generating code for NodeJS is slightly different. Idris outputs a
44+JavaScript file that can be directly executed via node.
45+
46+::
47+
48+ $ idris --codegen node hello.idr -o hello
49+ $ ./hello
50+ Hello world
51+
52+
5353
5454Third Party
5555============