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 /LICENSE | |
| parent | 8dc7fb147fb49294ccc4357b0c566b7e007c680f (diff) | |
| download | compcert-kvx-da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074.tar.gz compcert-kvx-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 'LICENSE')
0 files changed, 0 insertions, 0 deletions