diff options
| author | coqbot-app[bot] | 2020-12-29 19:05:11 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-29 19:05:11 +0000 |
| commit | 810e91530071159e27e89bf0ca6bc36c8bb1d034 (patch) | |
| tree | e364ea9b006d56f1ae1d28b21aa642bcb5d59c7b /dev/build | |
| parent | 942fb01934b02181fd3a88d80fc870f8d4900d2c (diff) | |
| parent | 627dcd739d67fdc4535af9ca0e36e65b3714f477 (diff) | |
Merge PR #13686: [refman] Clarify meaning of goal in documentation of instantiate.
Reviewed-by: jfehrle
Diffstat (limited to 'dev/build')
0 files changed, 0 insertions, 0 deletions