diff options
| author | Pierre-Marie Pédrot | 2020-04-16 22:04:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-16 22:04:28 +0200 |
| commit | 8ba8c68eeb8653896523b4bce9453f832c919899 (patch) | |
| tree | 612f54d6c7039492a35f0503c69201c84d775cb4 /doc/plugin_tutorial/tuto2/src/custom.ml | |
| parent | 6624276dce18978f5b9bd9c592a92195bccfb410 (diff) | |
| parent | 88b1f400ef05142a1f05cd7dcb34a4c682b7ab83 (diff) | |
Merge PR #12070: Ignore -native-compiler option when disabled
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/custom.ml')
0 files changed, 0 insertions, 0 deletions