diff options
| author | Pierre-Marie Pédrot | 2018-07-02 18:08:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-02 20:01:39 +0200 |
| commit | f3fa8071d78841630f2ec8657478e667f70afc16 (patch) | |
| tree | ab64b4540a24227390721b50cb10cc185c621e9b /kernel/modops.ml | |
| parent | 682368d0b8a4211dbeba8c2423f53d0448fd7d71 (diff) | |
Documenting the syntax changes.
Diffstat (limited to 'kernel/modops.ml')
0 files changed, 0 insertions, 0 deletions