mention the nuclear option

howto/gitlab.md

@@ -462,6 +462,10 @@ Other users, then can just run this command will rename `master` to
 
     git-branch-rename-remote
 
+Obviously, users without any extra data in their local repository can
+just destroy their local repository and clone a new one to get the
+correct configuration.
+
 Keep in mind that there may be a few extra steps and considerations to
 make when changing the name of a heavily used branch, detailed below.