From 22d8683c16e863dc44ef45d66a4530d8c63d2c30 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sun, 19 Apr 2020 20:03:49 +0200
Subject: forgotten extraction

---
 extraction/extraction.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'extraction')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index b102503b..18637336 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -224,4 +224,5 @@ Separate Extraction
    Floats.Float32.from_parsed Floats.Float.from_parsed
    Globalenvs.Senv.invert_symbol
    Parser.translation_unit_file
-   Compopts.optim_postpass.
+   Compopts.optim_postpass
+   Archi.has_notrap_loads.
-- 
cgit