diff options
| author | Maxime Dénès | 2016-09-28 15:28:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-28 15:28:51 +0200 |
| commit | 2c4f3c2bcf93d023b53a9f2ec6b151d4df696c84 (patch) | |
| tree | 2a8f3c92e40efe0eb5651c01bd3bf613bd68cf2c /kernel/cemitcodes.ml | |
| parent | 72c1fefcfb3f0dff02005034685f6b58ff84b3cc (diff) | |
| parent | 4b61c0693d453dd0026792185354d68ba1db9022 (diff) | |
Merge remote-tracking branch 'github/pr/232' into v8.6
Was PR#232: Fix the parsing of goal selectors.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions