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 /toplevel/coqtop_bin.ml | |
| 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 'toplevel/coqtop_bin.ml')
| -rw-r--r-- | toplevel/coqtop_bin.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml deleted file mode 100644 index 56aced92a..000000000 --- a/toplevel/coqtop_bin.ml +++ /dev/null @@ -1,2 +0,0 @@ -(* Main coqtop initialization *) -let () = Coqtop.start() |