diff --git a/Jenkinsfile b/Jenkinsfile index ce1faf4b31e..09a85bcc982 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -6,7 +6,7 @@ pipeline { } parameters { - choice(name: 'TARGET_PLATFORM', choices: ['r202403', 'r202406', 'r202409', 'latest'], description: 'Which Target Platform should be used?') + choice(name: 'TARGET_PLATFORM', choices: ['r202403', 'r202406', 'r202409', 'r202412', 'latest'], description: 'Which Target Platform should be used?') // see https://wiki.eclipse.org/Jenkins#JDK choice(name: 'JDK_VERSION', choices: [ '17', '21' ], description: 'Which JDK version should be used?') } diff --git a/xtext-r202412.target b/xtext-r202412.target new file mode 100644 index 00000000000..b62a202b178 --- /dev/null +++ b/xtext-r202412.target @@ -0,0 +1,79 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +