From 01f0c21c6d45d44b1fc78f1a41ea1cb8d1b550f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Feb 2015 14:54:37 +0100
Subject: coqc accepts -top option. Fixes bug #4043.

---
 tools/coqc.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5c7be41bec..7e822dbe36 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -121,7 +121,7 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
       as o) :: rem ->
 	begin
-- 
cgit v1.2.3