Beat Küng b190d98d6d Jenkinsfile: remove dev-guide metadata deployment
dev guide got merged with the user guide.
2021-01-20 10:03:00 -05:00
..
2019-10-01 10:35:28 -04:00