Skip to content

remove useless files #743

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

Merged
merged 1 commit into from
Dec 1, 2022
Merged

remove useless files #743

merged 1 commit into from
Dec 1, 2022

Conversation

umbynos
Copy link
Contributor

@umbynos umbynos commented Dec 1, 2022

Please check if the PR fulfills these requirements

  • The PR has no duplicates (please search among the Pull Requests
    before creating one)
    - [ ] Tests for the changes have been added (for bug fixes / features)
  • What kind of change does this PR introduce?

cleanup

  • What is the current behavior?

There are some old and useless files in the repo. These were the old files for the build pipeline. They are not required anymore since we swithced to github actions long time ago.

  • What is the new behavior?

🧹

  • Does this PR introduce a breaking change?

no

  • Other information:

@umbynos umbynos self-assigned this Dec 1, 2022
@umbynos umbynos merged commit 4372c8e into main Dec 1, 2022
@umbynos umbynos deleted the cleanup branch December 1, 2022 10:46
@per1234 per1234 added topic: infrastructure Related to project infrastructure type: imperfection Perceived defect in any part of project labels Dec 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
topic: infrastructure Related to project infrastructure type: imperfection Perceived defect in any part of project
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants