Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve docs and migrate to separate website #472

Merged
merged 31 commits into from
May 22, 2024
Merged

Improve docs and migrate to separate website #472

merged 31 commits into from
May 22, 2024

Conversation

FabijanC
Copy link
Contributor

Usage related changes

Development related changes

  • Now the development process also depends on Node/npm
    • Updated the executor Docker image in config.yml
  • Updated contribution guidelines with the content of the # Development section of README.md

Checklist:

  • Checked out the contribution guidelines
  • Applied formatting - ./scripts/format.sh
  • No linter errors - ./scripts/clippy_check.sh
  • No unused dependencies - ./scripts/check_unused_deps.sh
  • No spelling errors - ./scripts/check_spelling.sh
  • Performed code self-review
  • Rebased to the latest commit of the target branch (or merged it into my branch)
  • Updated the docs if needed, including the TODO section
  • Linked the issues resolvable by this PR - linking info
  • Updated the tests if needed; all passing - execution info

@FabijanC FabijanC merged commit 164a856 into main May 22, 2024
@FabijanC FabijanC deleted the website branch May 22, 2024 12:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Documentation should be ported to a separate site
2 participants