diff options
| author | Maxime Dénès | 2018-06-29 10:15:28 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-29 10:15:28 +0200 |
| commit | acbc42ad1da48be53456c0d41ec2e60ae2d6e642 (patch) | |
| tree | 997d7e949de3541111ec01708be973abb678f24b /Makefile.build | |
| parent | fc4f18c84bfc421dff55c77aa564abc1ea20f528 (diff) | |
| parent | 315aa093490d533e3d8db7a24bde78ed812c3b0d (diff) | |
Merge PR #7890: Inline a function from Quote used in setoid_ring.
Diffstat (limited to 'Makefile.build')
0 files changed, 0 insertions, 0 deletions