Adding command line for C codegen
Taken from: docs/tutorial/miscellany.rst
commit47387f6e015e610ff1cf914e27454ea499a4d70a
authorzenntenn <zenten@zenten.ca>
dateFri 11 Oct 2019, 11:26 (7 years ago)
parent5965fb1
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