diff options
| author | Pierre-Marie Pédrot | 2019-02-04 12:16:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 12:16:59 +0100 |
| commit | 019123cf911949480d300beba30b63db19c46b7b (patch) | |
| tree | fd61ecc206db85b0a03eb3c29428b73e5a3f962c /kernel/nativecode.ml | |
| parent | a5f260d6a397706fa91d2e128e9999d0c74b5739 (diff) | |
| parent | 9b39f65b25ff434cddda9a312eb40e9f099d298e (diff) | |
Merge PR #9461: Fix default goal selector error message.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions