diff options
| author | coqbot-app[bot] | 2020-08-27 14:03:35 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-27 14:03:35 +0000 |
| commit | 0e70c44e2dd19b7323b64b02578544424da95712 (patch) | |
| tree | 9829b770c29042cd24b31831d7aad1cb320eee16 /kernel/type_errors.ml | |
| parent | 871efc286594faebd34dd8735ee950c5a3a5b98b (diff) | |
| parent | cd7b346ec5485138d93bc6a0308b9b8176d6e71f (diff) | |
Merge PR #12850: Avoid running configure when plugins/ modified
Reviewed-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions