[crux-commits] ports/opt (3.3): Merge branch '3.2' into 3.3

commit 8e598eb2d12099a5e81d7b55db2b9f092fc283c6 Merge: 7f4b883 9903c20 Author: Juergen Daubert <jue@jue.li> Date: Thu Jan 19 10:48:38 2017 +0100 Merge branch '3.2' into 3.3