From 392b4fb9e94b5142441a79cb80f2e888429f0ef4 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 2 Oct 2023 19:11:42 +0200 Subject: [PATCH] Use settings.gradle to set project name --- README.md | 3 ++- build.gradle | 1 - settings.gradle | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) create mode 100644 settings.gradle diff --git a/README.md b/README.md index c533a1b..6058419 100644 --- a/README.md +++ b/README.md @@ -12,8 +12,9 @@ No original file is changed, but we added: * gradlew * gradlew.bat * gradle.properties.enc -* secring.gpg.enc * pubring.gpg.enc +* secring.gpg.enc +* settings.gradle Note to future Jens: After updating the sources the ```gradle patch``` task must be run. This modifies the sources. **Do not run the task multiple times!** diff --git a/build.gradle b/build.gradle index 8ee73f9..ae3af3e 100644 --- a/build.gradle +++ b/build.gradle @@ -6,7 +6,6 @@ sourceCompatibility = '1.7' project.version = '3.2.1-SNAPSHOT' project.group = 'de.hhu.stups' -project.archivesBaseName = 'rodin-eventb-ast' sourceSets { main { diff --git a/settings.gradle b/settings.gradle new file mode 100644 index 0000000..07405e3 --- /dev/null +++ b/settings.gradle @@ -0,0 +1 @@ +rootProject.name = "rodin-eventb-ast" -- GitLab