Closed matthid closed 9 years ago
I noticed that you already merged some commits manually, and now this has merge conflicts... Is there a reason to not use the github merge button?
Besides that It probably would be a good idea to test out travis with this pull request before merging! Did you enable travis for this project already? Once travis is enabled I can push the rebased branch and travis should start working...
@matthid Yes I had to fix this problem with ctags immediately a few days ago because it cause a big issue with analysis. Some projects we only analyze using the ctags methods because the language is not supported by doxygen.
No using the merge button is just habit of doing everything via cli. Perhaps one day I will have the courage to test out this button :)
I have not setup travis yet. Next thing on the list.
For this commit about fixing the fall back to ctags just forget it. I will take my fix and handle anything if it causes issues with the file based analysis.
Ah I see, so basically this is already done pretty much the same way, good to know :)
Hm even when merging via CLI I thought github would automatically close the pull request (I mean I opened them all on mitchell-updates branch so it makes no sense for github to leave them open until they are merged to the master branch). Either github waits for the commits to be in master OR your git cli parameters modify the commits somehow? There is actually a list of commands on the pull request page you should use (then github should notice the merge).
For travis: It should be as simple as logging in in travis with your github account and clicking enable on codeface, if anything doesn't work let me know!
See https://github.com/siemens/codeface/commit/1518a48ce3957d15c86d450fcc6e8ff154e7f236.
Please merge the travis pull request first!