diff options
author | Maxime Dénès <maxime.denes@inria.fr> | 2019-07-04 20:02:59 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-04 20:02:59 +0200 |
commit | da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074 (patch) | |
tree | 78320e4b422033d2b1a64937ccf00c6fe5ab748e /test/regression/builtins-arm.c | |
parent | 8dc7fb147fb49294ccc4357b0c566b7e007c680f (diff) | |
download | compcert-da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074.tar.gz compcert-da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074.zip |
Avoid relying on `Export` bug (#301)
The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
Diffstat (limited to 'test/regression/builtins-arm.c')
0 files changed, 0 insertions, 0 deletions