Correct official versioning in master branch (#2658)
According to the description at the top of gen_version.py and the
commit that introduced it, the "Official build" versioning is meant
to add 10000 to the number of commits since the last official release
when the build is in the master branch. However, because of the use
of "is" instead of "==", the comparison between the variable and
the string literal in the python script was never succeeding. The
"is" operator only succeeds when it compares two variables that
have been assigned the same variable or one has been assigned to
the other. For comparisons of contents, "==" should be used.