Development: Migrate documentation to docs.artemis.cit.tum.de

[ignacio-gn]

Checklist

General

• Language: I followed the guidelines for inclusive, diversity-sensitive, and appreciative language.
• I chose a title conforming to the naming conventions for pull requests.

Motivation and Context

The documentation of Artemis is going to be hosted on docs.artemis.cit.tum.de instead of the GitHubPages environment, ls1intum.github.io. This PR modifies the docs workflow to deploy the artifact on docs.artemis.cit.tum.de. It also replaces all occurrences of ls1intum.github.io in the repository to docs.artemis.cit.tum.de.

Description

On .github/workflows/docs.yml, the docs job was modified to not edit the built artifact for it to be deployed on GitHubPages. The deploy job was modified to download the artifact and upload it to docs.artemis.tum.de.

Repository-wide occurrences of ls1intum.github.io were changed to docs.artemis.cit.tum.de. This includes:

• Markdown files, including multiple READMEs and the pull request template,
• Comments/Javadoc that reference the documentation
• Elements in the web app that link to the documentation
• The baseURL attribute of the DocumentationButtonComponent and its test instance

Steps for Testing

The workflow has been tested together with the server-side configuration. This PR does not modify the functionality of Artemis.

[github-actions]

There hasn't been any activity on this pull request recently. Therefore, this pull request has been automatically marked as stale and will be closed if no further activity occurs within seven days. Thank you for your contributions.

[ignacio-gn]

The workflow has been succesfully tested and the server was configured. An (outdated) version of the documentation was deployed to https://docs.artemis.cit.tum.de using this workflow.