Get rid of pp.sed
commitb7d12118c972a1b01f558d6c8233e7803458b3ea
authormalc <moosotc@gmail.com>
Tue, 29 Nov 2016 06:19:32 +0000 (29 09:19 +0300)
committermalc <moosotc@gmail.com>
Tue, 29 Nov 2016 06:19:32 +0000 (29 09:19 +0300)
treeb5688237bce569f61740548ac60a18180f177293
parent92218bfe1cb759e67fcfa865c43499a9f5222f5e
Get rid of pp.sed

Idea and initial implementation - Nicolás Ojeda Bär.

(Todo: Shakefile.hs can be trimmed by removing the pp magic)
Shakefile.hs
build.sh
main.ml
pp.sed [deleted file]
wsi.ml
wsi.mli