diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:09:16 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:09:16 +0100 |
commit | 0c345d64d67c01c7b7a75bf23391b421f95c4fb7 (patch) | |
tree | f86b9a5c1093dfe66f744c86f8ed8ab6bae993d6 /toplevel/coqtop_bin.ml | |
parent | 16f93d201cf7e379d5acf533be20fed30bbc212c (diff) | |
parent | 17f9e85d9785b2ab77426e6d8644840fa7f37d85 (diff) |
Merge PR #6871: [build] Simpler byte/opt toplevel build.
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() |