aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/dune
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/dune')
-rw-r--r--extraction/dune11
1 files changed, 8 insertions, 3 deletions
diff --git a/extraction/dune b/extraction/dune
index ec44a53..12a6b8d 100644
--- a/extraction/dune
+++ b/extraction/dune
@@ -1,3 +1,8 @@
-(executable
- (name main)
- (flags (:standard -warn-error -A)))
+(executables
+ (flags (:standard -warn-error -A))
+ (names driver)
+ (libraries compcert))
+
+(install
+ (section bin)
+ (files (driver.exe as coqup)))