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(-)

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


From c68455771e65ae63be35a7f2b67e0c9931878758 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 26 May 2020 10:44:44 +0200
Subject: Fix worker handling of command-line options that are already included
 in initial state.

---
 stm/asyncTaskQueue.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 1a232ac93a..a8088dae36 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -130,18 +130,23 @@ module Make(T : Task) () = struct
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
           | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv"
+          | "-require-import" | "-require-export" | "-ri" | "-re"
+          | "-load-vernac-object"
+          | "-set" | "-unset" | "-compat" | "-mangle-names" | "-diffs" | "-w"
           | "-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"
           | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl ->
           set_slave_opt tl
+        (* Options to discard: 2 arguments *)
+        | ( "-rifrom" | "-refrom" | "-rfrom"
+          | "-require-import-from" | "-require-export-from") :: _ :: _ :: tl ->
+           set_slave_opt tl
         (* We need to pass some options with one argument *)
-        | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
-          | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from"
-          | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object"
-          | "-w" | "-color" | "-init-file"
-          | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
-          | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
+        | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir"
+          | "-color" | "-init-file"
+          | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel"
+          | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
           x :: a :: set_slave_opt tl
         (* We need to pass some options with two arguments *)
         | ( "-R" | "-Q" as x) :: a1 :: a2 :: tl ->
-- 
cgit v1.2.3


From 850e3634b91a30a7510fdea9ac970775a79bd64b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 26 May 2020 12:07:48 +0200
Subject: Fix usage of -rifrom, -refrom.

---
 toplevel/usage.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e69b21a195..732ad05b26 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -50,10 +50,10 @@ let print_usage_common co command =
 \n  -require-export lib, -re lib\
 \n                         load and transitively import Coq library lib\
 \n                         (equivalent to Require Export lib.)\
-\n  -require-import-from root lib, -rifrom lib\
+\n  -require-import-from root lib, -rifrom root lib\
 \n                         load and import Coq library lib\
 \n                         (equivalent to From root Require Import lib.)\
-\n  -require-export-from root lib, -refrom lib\
+\n  -require-export-from root lib, -refrom root lib\
 \n                         load and transitively import Coq library lib\
 \n                         (equivalent to From root Require Export lib.)\
 \n\
-- 
cgit v1.2.3