diff options
| author | Emilio Jesus Gallego Arias | 2019-06-11 02:16:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:14 +0200 |
| commit | 75e7c5b596d2a3e9b54e84788a15299568792584 (patch) | |
| tree | 6b326ec3279535bcad3f5bcbe0080679b2621dfb /dev/ci/docker | |
| parent | 0ad30b6fce3eb757d06808e160a4c92e45686072 (diff) | |
[equations] [proof] Remove duplicate shrink function.
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions