From 2edd93eec8e9bd83da2bbb77a904bb290ee7adf3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 4 Feb 2021 12:25:17 +0100
Subject: Remove deprecated -inputstate command line argument

Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
---
 sysinit/coqargs.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'sysinit/coqargs.mli')

diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index aef50193f2..4dd3f32ad0 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -60,8 +60,6 @@ type coqargs_pre = {
 
   load_vernacular_list : (string * bool) list;
   injections  : injection_command list;
-
-  inputstate  : string option;
 }
 
 type coqargs_query =
-- 
cgit v1.2.3