From e8419bac30ab98527ec6b15d5a0f5c1035539ca5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 12 Feb 2019 02:41:00 +0100 Subject: [library] Remove `-boot` option. The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575 --- test-suite/bugs/closed/bug_5198.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/bug_5198.v b/test-suite/bugs/closed/bug_5198.v index 5d4409f89b..4f24189d3f 100644 --- a/test-suite/bugs/closed/bug_5198.v +++ b/test-suite/bugs/closed/bug_5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from -- cgit v1.2.3