merge github/master into v8.0-pre

since some large files were committed by mistake, and cleaning up these
large files we modified the history from 0ea9c829 (including commits that
had been merged in but were not relevant), so to make github side branch
clean and ensure that the pull request still working, we merge the
github master branch again

Change-Id: I25e2bbed6ff472a6f76d32fe6d7256360d15a253

Author: lykling