aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop_bin.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 13:09:16 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 13:09:16 +0100
commit0c345d64d67c01c7b7a75bf23391b421f95c4fb7 (patch)
treef86b9a5c1093dfe66f744c86f8ed8ab6bae993d6 /toplevel/coqtop_bin.ml
parent16f93d201cf7e379d5acf533be20fed30bbc212c (diff)
parent17f9e85d9785b2ab77426e6d8644840fa7f37d85 (diff)
Merge PR #6871: [build] Simpler byte/opt toplevel build.
Diffstat (limited to 'toplevel/coqtop_bin.ml')
-rw-r--r--toplevel/coqtop_bin.ml2
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()