diff options
author | Matej Kosik <matej.kosik@inria.fr> | 2016-10-18 11:33:41 +0200 |
---|---|---|
committer | Matej Kosik <matej.kosik@inria.fr> | 2016-10-19 13:48:52 +0200 |
commit | b403e0224ba502c0cd80702eca08405aa6de0828 (patch) | |
tree | f4daf3f122d04a43f8ea11248ca880997a9b170a /tactics | |
parent | 7b4dbbb83e3da2fe716dacad627ddd3497653f07 (diff) |
COMMENT: was added to "Nameops.increment_suffix".
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions