mirror of
https://github.com/boostorg/config.git
synced 2026-07-08 01:10:57 +02:00
6393b50d79
Rename mips1 to mips and alias mips1 to mips
Rename mips1 to mips and alias mips1 to mips