The question here is basically, should we do periodic merges from master to a feature branch? My take is that this is not usually helpful when the merge would succeed without intervention. I don't know how common it is that this particular merge needs help. Repeated merges between branches that don't have any merge conflicts just confuse the history.