diff options
| author | Enrico Tassi | 2020-11-23 12:08:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-27 14:29:22 +0100 |
| commit | d309974601ccb55f2339a4ea12d72428402ed195 (patch) | |
| tree | 9984462b0f8fc041c822d267efa7aba696068bdc /kernel/type_errors.ml | |
| parent | 7f3c46acc937eb9257c29b5881e5a8b17b28cd48 (diff) | |
[RM] script to notify "platform" projects to tag
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions