diff options
| author | coqbot-app[bot] | 2020-08-26 03:25:56 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-26 03:25:56 +0000 |
| commit | 48bd6534edc6b3e6b9309a443fabbb869f6957f9 (patch) | |
| tree | 3af3c09416a4cb818401846a13244eee643c9aab /dev/include | |
| parent | e01f9df8aa68ecae26bce15544b7244ced1b2be5 (diff) | |
| parent | 2a703ebef927b1eaab43279efef4dde8c99c6384 (diff) | |
Merge PR #12884: Documentation of coq_makefile: fix name of installation dir + help on using option -f
Reviewed-by: jfehrle
Ack-by: herbelin
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions