diff options
| author | stuebinm | 2021-09-02 23:31:39 +0200 |
|---|---|---|
| committer | stuebinm | 2021-09-03 00:02:16 +0200 |
| commit | ad514f56b6cda288e605c44990ef16d30e6dee53 (patch) | |
| tree | bec6de5f4bdabf432c7045394af15ba96f525546 /isabelle-licence | |
| parent | 715001ba92799839afc97d92c9f0a79924085a69 (diff) | |
remove grmtools
the parser using grmtools was way oversized for just doing escape
sequences, and only really existed since I wanted to play around with
it.
The new implementation depends on no external crates, uses just an iter
wrapped into a nicely composable function, and appears to be exactly
equivalent (but faster).
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions