aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-02-06 16:53:12 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2017-02-06 16:53:12 +0100
commit8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed (patch)
tree43e89a45ed321081cbcaaac06165a7e62b84a34b /driver
parent9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff)
parent4afaf8c23274752c8a6067bd785e114578068702 (diff)
downloadcompcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.tar.gz
compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.zip
Merge branch 'elaboration-of-attributes'
Diffstat (limited to 'driver')
-rwxr-xr-xdriver/Driver.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 3219b7b7..9d5ed3b3 100755
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -540,6 +540,7 @@ let _ =
| _ -> assert false
end;
Builtins.set C2C.builtins;
+ Cutil.declare_attributes C2C.attributes;
CPragmas.initialize();
parse_cmdline cmdline_actions;
DebugInit.init (); (* Initialize the debug functions *)