javapathfinder / jpf-wiki-sync Goto Github PK

A recent change could not be merged; this should be investigated.

The current setup pushes accepted PRs on this repository to the wiki of jpf-core. However, the reverse direction is not supported. A cron job could be a solution.

However, it's actually not straightforward to pull the changes from the hidden wiki repo to our wiki repository jpf-wiki-sync, via cron.
This is because Travis only allows us to configure to run nightly builds in cron; i.e., it runs the normal build that it would otherwise also run whenever a change is pushed. For our purpose, this is not very useful.
The .travis.yml script we have pushes the changes from jpf-wiki-sync to the wiki of jpf-core. This makes sense for normal changes (merged pull requests to the wiki repo): we want them to be visible on the wiki page of jpf-core.
However, the cron should do the reverse, to merge changes people sometimes make on the wiki web interface: it should pull changes from the wiki of jpf-core, and merge them into master on jpf-wiki-sync. If not successful, it would be good to have an error message; otherwise the script should be quiet.

It is possible in theory to do this with .travis.yml, by checking if environment variable TRAVIS_EVENT_TYPE is set to "cron". However, getting all this to work well according to the criteria above, will take some work.

Perhaps someone can find an example template script, so we simply have to adapt it?

In Eclipse-Plugin.md there is a link pointing to https://github.com/javapathfinder/jpf-wiki-sync/blob/master/install/eclipse-jpf

It is possible that the current merge script only works if I accept a pull request (or push something), as it tries to set the user name to my github account, to use my github token.
This solution is not very elegant in any case; is it possible to use a group account to merge the data? Does anyone know github/Travis well enough to help fixing this?