[galaxy-commits] galaxy-dist commit 1ebd342fb4eb: branch merge