Skip to content
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

review chore: Add a script to update pom.xml for running pit-descartes #1820

Merged
merged 7 commits into from
Jan 31, 2018

Conversation

surli
Copy link
Collaborator

@surli surli commented Jan 12, 2018

This script intends to be used only in jenkins CI to update pom.xml before running pit-descartes as the plugin is not yet released.

@monperrus
Copy link
Collaborator

could we host this experimental stuff in Jenkins or Gakoci directly?

@surli
Copy link
Collaborator Author

surli commented Jan 15, 2018

The script is now available in http://spoon.gforge.inria.fr/jenkins/pit-descartes/

@surli surli closed this Jan 15, 2018
@surli surli reopened this Jan 18, 2018
@surli
Copy link
Collaborator Author

surli commented Jan 18, 2018

I made a mistake: the code of http://spoon.gforge.inria.fr/jenkins/ is replaced by doc/jenkins automatically at each deployment.
I propose then to move the content of this PR inside doc/jenkins/spit-descartes: + it guarantees to keep a version of those files in the repo.

@surli surli changed the title chore: Add a script to update pom.xml for running pit-descartes WiP chore: Add a script to update pom.xml for running pit-descartes Jan 18, 2018
@surli surli changed the title WiP chore: Add a script to update pom.xml for running pit-descartes review chore: Add a script to update pom.xml for running pit-descartes Jan 22, 2018
@surli
Copy link
Collaborator Author

surli commented Jan 22, 2018

The job is now running and working.

@monperrus monperrus merged commit 8ede7d2 into INRIA:master Jan 31, 2018
@monperrus
Copy link
Collaborator

thanks!

@surli surli deleted the auto-update-pom-for-pit-descartes branch January 31, 2018 10:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants