Skip to content
Snippets Groups Projects

Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`

Merged Robbert Krebbers requested to merge robbert/1_1_1_2 into master
Compare changes
  • Side-by-side
  • Inline
Files
3
Loading