aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-09-16 11:03:40 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-09-22 16:00:31 +0200
commitd32955030937937706b71a96dc6584800f0b8722 (patch)
treed82b440a150f3339715d9f0a208966ee66219a65 /configure
parent9e30fa95607cf357ab7c18a4773edf6b6f84c7d7 (diff)
downloadcompcert-kvx-d32955030937937706b71a96dc6584800f0b8722.tar.gz
compcert-kvx-d32955030937937706b71a96dc6584800f0b8722.zip
Refactor clightgen
Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure4
1 files changed, 2 insertions, 2 deletions
diff --git a/configure b/configure
index b342b143..10f60262 100755
--- a/configure
+++ b/configure
@@ -770,7 +770,7 @@ S backend
S cfrontend
S driver
S debug
-S exportclight
+S export
S cparser
S extraction
@@ -781,7 +781,7 @@ B backend
B cfrontend
B driver
B debug
-B exportclight
+B export
B cparser
B extraction
EOF