Manual would make more sense because we don't want a stable master to be
rebuilt every time we push to the dev branch. Unless Jenkins can kick off
that build only when we push to master.
Raff
On Oct 29, 2015 2:23 PM, "James Cummings"
Would this be a manual job that we kick off only when releasing? Or one that happens each time?
-James
On 29/10/15 12:23, Martin Holmes wrote:
I've just changed my Jinks to build dev branches. However, this now means we have no Jenkins build that we can use as a distribution source when we do a release. We will need to add another job, I think.
Cheers, Martin
On 2015-10-29 10:33 AM, Hugh Cayless wrote:
To switch to work on the dev branch, you should be able to just:
git fetch git checkout dev
Future pushes should be to dev, so
git push origin dev
You need to do this in both the TEI and Stylesheets repos.
Thanks all, Hugh
-- Dr James Cummings, James.Cummings@it.ox.ac.uk Academic IT Services, University of Oxford -- tei-council mailing list tei-council@lists.tei-c.org http://lists.lists.tei-c.org/mailman/listinfo/tei-council
PLEASE NOTE: postings to this list are publicly archived