Linus Heckemann 637701b604 rename build-extra-platforms -> extra-platforms ...

also document it

2018-03-16 22:50:27 +00:00

..

manual

rename build-extra-platforms -> extra-platforms

2018-03-16 22:50:27 +00:00