New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix typo in 'bibliograph' #2818
Conversation
Can someone explain what's going on here? When I look at master, the fix is already in place. |
That was due to henrikt-ma-patch-4-1 which was merged through #2803 (to master). |
Me neither, but what really puzzles me is why GitHub says that this branch still contains a change that can be applied to master: https://github.com/modelica/ModelicaSpecification/pull/2818/files |
My assumption is that you for unknown reason made two branches with the same contents; and some checks that the change isn't already there are done later. |
Btw, @henrikt-ma you might wanna avoid creating PR branches on the main repo but in your fork instead. Also clean up merged branches afterwards ;-) |
Yes! Would be appreciated. |
b94ed85
to
23c6c8f
Compare
Rebasing and force-pushing that branch auto-closes the PR - nice! |
Sure, cleaning up branches is what made me find this one. I am also generally happy about the idea of branch hygiene in the central repo. It is the convenient GitHub online editing that has tricked me into creating all these branches for changes so small that the branches are easily forgotten after merging. Automatic cleanup makes perfect sense for this type of branches! Now, does this mean that it becomes ok to keep creating central repo branches by GitHub online editing directly on the central repo? |
It would still be preferable to avoid it. However, as I understand it GitHub currently doesn't have good support for creating such branches in a local repository. |
Alternatively use an editor with GitHub integration where you can simply create PR and follow them up from within the editor and which then also has LaTeX support. One I can recommend here is VSCode and the integration is shown here: https://code.visualstudio.com/docs/editor/github |
Trying to clean up no longer needed branches, and I don't understand why GitHub still says the commit on this branch isn't present on master…