diff options
| author | coqbot-app[bot] | 2020-12-03 13:59:36 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-03 13:59:36 +0000 |
| commit | afbc39d8c4f24e2e8ccda0fcb861fb947f3f4c71 (patch) | |
| tree | a8be7066f13772bc04d54e92c3f9f408f1693249 /doc/plugin_tutorial/tuto2/Makefile | |
| parent | a88568e751d63d8db93450213272c8b28928dbf2 (diff) | |
| parent | 056245e24411c3f410d3e91897ad8ce97bc59587 (diff) | |
Merge PR #13548: Move *_with_full_binders variants out of the kernel.
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'doc/plugin_tutorial/tuto2/Makefile')
0 files changed, 0 insertions, 0 deletions