Skip to content
Snippets Groups Projects

Resolve "Renaming of Nonterminal Does Not Rename All Occurences"

Merged Resolve "Renaming of Nonterminal Does Not Rename All Occurences"
bugfix/nonterminal-renaming into main
Merged Johannes Mey requested to merge bugfix/nonterminal-renaming into main
Viewing commit 9eadce92
Prev Next
Show latest version
1 file
+ 6
− 0
Compare changes
  • Side-by-side
  • Inline
.gitlab-ci.yml
+ 6
− 0
@@ -4,6 +4,12 @@ stages:
@@ -4,6 +4,12 @@ stages:
- jar
- jar
- deploy
- deploy
 
test:
 
image: openjdk:11
 
stage: test
 
script:
 
- ./gradlew --continue --console=plain --info runPluginVerifier
 
jar:
jar:
image: openjdk:11
image: openjdk:11
stage: jar
stage: jar