aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-10-03 20:33:11 +0100
committerYann Herklotz <git@yannherklotz.com>2023-04-27 11:53:24 +0100
commit01c2e94a38f91af008e21a7be998da2db34ade03 (patch)
treed082eccc3d6d09626660544ced48b03ab18dd233
parent4884a324ed0fa3a8602777bdb49580e801ff6f5b (diff)
downloadcompcert-01c2e94a38f91af008e21a7be998da2db34ade03.tar.gz
compcert-01c2e94a38f91af008e21a7be998da2db34ade03.zip
Fix dune file as well
-rw-r--r--dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/dune b/dune
index 9d7272fc..2acf499d 100644
--- a/dune
+++ b/dune
@@ -1 +1 @@
-(dirs :standard \ aarch64 arm x86_32 riscV powerpc extraction)
+(dirs :standard \ aarch64 arm x86_32 riscV powerpc extraction x86 x86_64)