src/Pure/Admin/jenkins.scala
changeset 65703 cead65c19f2e
parent 65674 23897f5d885d
child 65736 2e7230b66a32
equal deleted inserted replaced
65702:7c6a91deb212 65703:cead65c19f2e