Hi everyone, I have added functionality to allow Github pull requests (PRs) to be merged directly. The default branch in Github (and the default for PR merges) is now called "sf-auto-merge" ... and anything pushed to this branch is automatically pushed to SourceForge (unless there are conflicts).
The master branch on Github directly mirrors the one in SourceForge. Conflicts on push to SourceForge can be solved entirely on Github by merging the master branch into sf-auto-merge. Best wishes, Stian Grenborgen
_______________________________________________ Freecol-developers mailing list Freecol-developers@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/freecol-developers
