diff options
author | 2019-02-06 07:24:25 -0500 | |
---|---|---|
committer | 2019-02-06 07:24:25 -0500 | |
commit | 4a85cdbc0796afd2e70a7daf30967dfa2fadbafd (patch) | |
tree | 76432c8d8a20e646d231e9de12c4a196588cd886 /pretyping/detyping.ml | |
parent | 4bf1d996c98a37c312c5dddf418316d77086e9c2 (diff) |
Update fix-bytecode-build.patch to latest version
The fix-bytecode-build.patch in previous commits works fine for
building and testing, but installation still fails on bytecode
platforms – the system tries to install .cmx files that don’t exist.
Update fix-bytecode-build.patch to the latest version from Gaëtan
Gilbert, which corrects the installation targets.
Diffstat (limited to 'pretyping/detyping.ml')
0 files changed, 0 insertions, 0 deletions