Remove java rts from idris.cabal
commit5d5c6132c63dbe6ef1d6184aaa7ab532bcbfd341
authorJan Bessai <Jan.Bessai@tu-dortmund.de>
dateTue 16 Jul 2013, 22:18 (13 years ago)
parentc5d5884
idris.cabal−5
@@ -72,7 +72,6 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
7272 rts/*.c rts/*.h rts/Makefile
7373 llvm/*.c llvm/Makefile
7474 js/*.js
75− java/src/main/java/org/idris/rts/*.java
7675 java/*.xml
7776
7877 Makefile
@@ -234,10 +233,6 @@ source-repository head
234233 type: git
235234 location: git://github.com/edwinb/Idris-dev.git
236235
237−Flag Java
238− Description: Build the Java RTS
239− Default: False
240−
241236Flag NoEffects
242237 Description: Do not build the effects package
243238 Default: False