1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sun, 11 Aug 2019 18:33:23 +0200
Subject: Ignore .pc directory when building
Forwarded: https://github.com/coq/coq/issues/11266
---
Makefile | 1 +
1 file changed, 1 insertion(+)
Index: coq/Makefile.make
===================================================================
--- coq.orig/Makefile.make 2020-08-21 13:17:25.355954280 +0200
+++ coq/Makefile.make 2020-08-21 13:17:25.355954280 +0200
@@ -53,6 +53,7 @@
-name '.*' -type d -o \
-name '_darcs' -o \
-name 'debian' -o \
+ -name '.pc' -o \
-name "$${GIT_DIR}" -o \
-name '_build' -o \
-name '_build_ci' -o \
|
