mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-13 05:48:39 +03:00
1f0ca85678
The output directory was previously called the executable directory, but I changed it because the output is not always an executable (depending on the code generator). The code generators can now distinguish between where to place the (temporary) build files and the resulting output files. |
||
---|---|---|
.. | ||
app | ||
backends | ||
faq | ||
ffi | ||
image | ||
listing | ||
proofs | ||
reference | ||
tutorial | ||
typedd | ||
updates | ||
conf.py | ||
index.rst |