diff options
| author | Maxime Dénès | 2020-09-28 09:15:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-28 09:15:49 +0200 |
| commit | 424ae427197126a2fcbd5f07eaa181fb6f81ad84 (patch) | |
| tree | c29f6c916f25da23465b2932710f0b2a01002335 /interp/notation.ml | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
CI script wrapper now requires Python
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions