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 5d1ca8a9
Prev Next
Show latest version
1 file
+ 2
− 2
Compare changes
  • Side-by-side
  • Inline
gradle.properties
+ 2
− 2
@@ -3,7 +3,7 @@
@@ -3,7 +3,7 @@
pluginGroup = org.jastadd
pluginGroup = org.jastadd
pluginName = JastAdd
pluginName = JastAdd
pluginVersion = 0.2.0
pluginVersion = 0.3.0
# See https://plugins.jetbrains.com/docs/intellij/build-number-ranges.html
# See https://plugins.jetbrains.com/docs/intellij/build-number-ranges.html
# for insight into build numbers and IntelliJ Platform versions.
# for insight into build numbers and IntelliJ Platform versions.
@@ -15,7 +15,7 @@ pluginUntilBuild = 212.*
@@ -15,7 +15,7 @@ pluginUntilBuild = 212.*
pluginVerifierIdeVersions = 2021.1.1, 2021.1.2, 2021.1.3, 2021.2.3
pluginVerifierIdeVersions = 2021.1.1, 2021.1.2, 2021.1.3, 2021.2.3
platformType = IC
platformType = IC
platformVersion = 2021.1.1
platformVersion = 2021.2.3
platformDownloadSources = true
platformDownloadSources = true
# Plugin Dependencies -> https://plugins.jetbrains.com/docs/intellij/plugin-dependencies.html
# Plugin Dependencies -> https://plugins.jetbrains.com/docs/intellij/plugin-dependencies.html