diff options
| author | Pierre Roux | 2020-10-28 10:32:58 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | 36ac26532028bfc6f84e4dfc849b51f42a3d8286 (patch) | |
| tree | 9a8057cf3171c7b8fcf1ca2aa452cddb3d14e0fc /plugins/syntax/string_notation.mli | |
| parent | e3593abd322acb59c512b5f2f776091546b38887 (diff) | |
Rename Dec and HexDec to Decimal and Hexadecimal
As noted by Hugo Herbelin, Dec is rather used for "decidable".
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions