diff options
| author | Enrico Tassi | 2015-02-04 14:31:57 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-04 14:31:57 +0100 |
| commit | 00853ca988d304af5b41834ee6b5766532233349 (patch) | |
| tree | af6a5dee8ee9ffd9567ceea4ddcbd46b9b981273 /dev | |
| parent | ab97dd2c8d49e59b7fb623e1fe9606395a176187 (diff) | |
Tactic Notation: use stable unique key for notations (Close: 3970)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions