From 2d9988d834804b577d934d1af662f9f8924f9322 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 26 May 2020 10:45:15 +0200
Subject: Remove command-line options that do not exist anymore.

---
 stm/asyncTaskQueue.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'stm/asyncTaskQueue.ml')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 87d844edb3..1a232ac93a 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -130,7 +130,6 @@ module Make(T : Task) () = struct
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
           | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv"
-          | "-compile" | "-compile-verbose"
           | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j"
           | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience"
           | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold"
-- 
cgit v1.2.3