From 324a90078a47e469e4b185cfc6333a741cf48dc2 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 26 Jul 2017 20:00:07 +0200
Subject: Enrich test file 4720.v with a compilation test of the extracted code

---
 test-suite/bugs/closed/4720.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v
index 9265b60c17..704331e784 100644
--- a/test-suite/bugs/closed/4720.v
+++ b/test-suite/bugs/closed/4720.v
@@ -44,3 +44,7 @@ Recursive Extraction WithMod.
 Recursive Extraction WithDef.
 
 Recursive Extraction WithModPriv.
+
+(* Let's even check that all this extracted code is actually compilable: *)
+
+Extraction TestCompile WithMod WithDef WithModPriv.
-- 
cgit v1.2.3