diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 06:30:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-05 14:48:42 +0100 |
| commit | 17f9e85d9785b2ab77426e6d8644840fa7f37d85 (patch) | |
| tree | 0984400b6fb6776477df2ae74a02e5d2e8bdfa33 /pretyping/reductionops.mli | |
| parent | 15331729aaab16678c2f7e29dd391f72df53d76e (diff) | |
[build] Simpler byte/opt toplevel build.
Instead of playing static linking games, we just ship two different
top-level files depending on whether we want to enable `Drop` support
[bytecode case] or not.
The savings of the old approach [1 line of code] were not worth the
complexities of the linking hack.
Diffstat (limited to 'pretyping/reductionops.mli')
0 files changed, 0 insertions, 0 deletions