diff options
| author | Enrico | 2016-05-18 13:38:51 +0200 |
|---|---|---|
| committer | Enrico | 2016-05-18 13:38:51 +0200 |
| commit | aa13fe8081c0d28478e5464bfdb52e44b1df6945 (patch) | |
| tree | 0eff554ade7ed76339b532954674bf4766fdd8e6 /mathcomp/Make | |
| parent | d9cecc8f2f1d38947e4889b996c42b26c08f9be1 (diff) | |
| parent | 1327aada8c68d8ba5ff97b22f4296a3cd5a33f6e (diff) | |
Merge pull request #46 from ppedrot/partial-fix
Fix compilation after the change of API in Tactics.
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions