From a1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 8 Sep 2022 16:10:20 +0200 Subject: test/export: use the standard headers from ../../runtime/include Just like in the other test/ directories. --- test/export/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/export/Makefile b/test/export/Makefile index d1228bf9..5cad730d 100644 --- a/test/export/Makefile +++ b/test/export/Makefile @@ -13,7 +13,7 @@ endif COQINCLUDES += -R ./clight compcert.test.clight COQINCLUDES += -R ./csyntax compcert.test.csyntax -CLIGHTGEN=../../clightgen +CLIGHTGEN=../../clightgen -stdlib ../../runtime COQC=coqc # Regression tests in the current directory -- cgit