I noticed that after running smt run repeat , the git repository is brought back at the commit present before the smt command, but in a detached head state. I am not sure which should be the expected behaviour actually, because there is still the possibility that the repository was in a detached state already before the smt run repeat command. Looking at the discussion in http://stackoverflow.com/a/3965714/1136458 , maybe the checkout command should use the branch name (not the commit hash) if the original state of the repository was at the tip of a branch ? Or maybe just explicitly warn the user that now they are in a detached state?
I noticed that after running smt run repeat , the git repository is brought back at the commit present before the smt command, but in a detached head state. I am not sure which should be the expected behaviour actually, because there is still the possibility that the repository was in a detached state already before the smt run repeat command. Looking at the discussion in http://stackoverflow.com/a/3965714/1136458 , maybe the checkout command should use the branch name (not the commit hash) if the original state of the repository was at the tip of a branch ? Or maybe just explicitly warn the user that now they are in a detached state?