We need libs/Makefile too!
I should definitely go home.
commit873e824422b66922c83536b8eb764a1a0ad66696
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 20 Nov 2013, 18:38 (13 years ago)
parent2d68066
idris.cabal+2−1
@@ -66,6 +66,8 @@ Extra-source-files:
6666 rts/*.h
6767 rts/Makefile
6868
69+ libs/Makefile
70+
6971 libs/base/base.ipkg
7072 libs/base/*.idr
7173 libs/base/Control/*.idr
@@ -86,7 +88,6 @@ Extra-source-files:
8688 libs/effects/Effect/*.idr
8789 libs/effects/*.idr
8890
89−
9091 libs/javascript/*.idr
9192 libs/javascript/JavaScript/*.idr
9293 libs/javascript/Makefile