From 0f24d6d6c6a61c9a3f090649003df7daabff4d65 Mon Sep 17 00:00:00 2001
From: Chimrod <>
Date: Fri, 3 Nov 2023 19:00:34 +0100
Subject: Removed the interractive command line option

---
 bin/args.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'bin/args.mli')

diff --git a/bin/args.mli b/bin/args.mli
index 1a063fc..5231cae 100644
--- a/bin/args.mli
+++ b/bin/args.mli
@@ -1,6 +1,6 @@
 type filters = { level : Qsp_syntax.Report.level option }
 
-type t = { reset_line : bool; filters : filters; interractive : bool }
+type t = { reset_line : bool; filters : filters }
 (** All the arguments given from the command line *)
 
 val parse : unit -> string list * t
-- 
cgit v1.2.3