diff options
| author | Enrico | 2018-04-12 17:14:20 +0200 |
|---|---|---|
| committer | GitHub | 2018-04-12 17:14:20 +0200 |
| commit | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (patch) | |
| tree | b95ac156d027c91f2103d33b46dbf5d2bcae33b8 /mathcomp/Make | |
| parent | c17414bbef21bb3d0b96ee004c29ef7d56e55e2e (diff) | |
| parent | ac07a76ee257c535b5686b49fd14c6d1e370cc9a (diff) | |
Merge pull request #190 from gares/anon-fix
ssrnat: don't use `fix n` but rather `fix name n`
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions