Merge pull request #4767 from zenntenn/patch-1
Adding command line for C codegen
commit3257106a6ceb07ddee78e28ddddeab18f4e15f2d
authorNiklas Larsson <metaniklas@gmail.com>
dateMon 21 Oct 2019, 13:30 (7 years ago)
parent5965fb147387f6
docs/reference/codegen.rst+7
@@ -16,6 +16,13 @@ Official Backends
1616C Language
1717----------
1818
19+The default target of Idris is C. In order to view the generated C code, compile via:
20+
21+::
22+
23+ $ idris hello.idr -S -o hello.c
24+
25+
1926Javascript
2027----------
2128