Merge cimgui docking_inter branch into master and re-generate

merge_branch.sh

#!/bin/bash
set -ex

to_merge="${1:-docking_inter}"
imgui_branch="${2:-master}"

git merge --no-ff --no-commit "$to_merge" || true  # Always fails
# But double-check that we really ended up in a merge status
git rev-list -1 MERGE_HEAD
# Reset everything to be like the merged branch
git checkout "$to_merge" .
# Update imgui
git submodule update
(
    cd imgui
    git fetch
    # Update to corresponding master-based version of imgui
    git checkout $(git merge-base HEAD "origin/$imgui_branch")
)
# Re-generate
(
    cd generator
    ./generator.sh
)
git add -u
# Commit with default commit message
GIT_EDITOR=true git merge --continue