From 1cffe2f00d91bc9739b40887eb36f4bbad761c5f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Feb 2021 19:25:53 +0100
Subject: [coqc] Don't allow to pass more than one file to coqc

This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.

Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.

(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
---
 test-suite/bugs/closed/PLACEHOLDER.v | 0
 test-suite/bugs/closed/bug_4836.v    | 2 +-
 2 files changed, 1 insertion(+), 1 deletion(-)
 delete mode 100644 test-suite/bugs/closed/PLACEHOLDER.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 9aefb10172..62d39619b0 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
+(* Placeholder file for directory / file test *)
-- 
cgit v1.2.3