diff options
| author | Enrico Tassi | 2021-01-06 14:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | b9bac1d7ef4a4c06ebe842ffd9aac322186a65d3 (patch) | |
| tree | f29e86bd00ca4ad1ec0d4d1e45b1b523957a665a /sysinit/coqargs.mli | |
| parent | 4c4d6cfacf92b555546055a45edc19b68245b83c (diff) | |
[coqc] move -output-context from sysinit/coqargs to coqc proper
Diffstat (limited to 'sysinit/coqargs.mli')
| -rw-r--r-- | sysinit/coqargs.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index ebf367270d..acf941f730 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -74,7 +74,6 @@ type coqargs_main = type coqargs_post = { memory_stat : bool; - output_context : bool; } type t = { |