From 146415fb624c182493d46413d738a3c2c3f47e02 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 13 Nov 2020 12:03:19 +0100
Subject: [CI] Update coq_makefile

---
 test-suite/coq-makefile/plugin2/run.sh | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite/coq-makefile/plugin2')

diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 1e2bd979b3..f69e8c1b8c 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp"
 sort > desired <<EOT
 .
 ./test
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
 ./test/test.glob
 ./test/test.cmi
 ./test/test.cmx
@@ -23,4 +27,5 @@ sort > desired <<EOT
 ./test/test.v
 ./test/test.vo
 EOT
+(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
 exec diff -u desired actual
-- 
cgit v1.2.3