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_opt_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_opt_bin.ml')
-rw-r--r-- | toplevel/coqtop_opt_bin.ml | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml index 410b4679a..ea4c0ea52 100644 --- a/toplevel/coqtop_opt_bin.ml +++ b/toplevel/coqtop_opt_bin.ml @@ -1,3 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = Mltop.remove () -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() |