diff options
| author | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
| commit | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (patch) | |
| tree | caf236823940843f1609112162801250bf5dfdb6 /engine | |
| parent | 06b820259989a59080d0dc68bf0c633994fe221f (diff) | |
| parent | 57bc1b7921da4ae54ee5d3b999351f297556fd65 (diff) | |
Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions