Skip to content

change: remove remote dev docs#218

Merged
micbar merged 1 commit intomainfrom
dev-docs
Apr 9, 2025
Merged

change: remove remote dev docs#218
micbar merged 1 commit intomainfrom
dev-docs

Conversation

@micbar
Copy link
Copy Markdown
Member

@micbar micbar commented Apr 9, 2025 •
edited
Loading

Remove Remote Dev Docs

  • Remove the CI "Fetch Devdocs" step
  • Remove the batchfile

@micbar micbar requested review from AlexAndBear and Copilot April 9, 2025 14:10
Copilot AI reviewed Apr 9, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot reviewed 1 out of 2 changed files in this pull request and generated no comments.

Files not reviewed (1)
  • .batchfile: Language not supported

@micbar micbar merged commit ae9eb40 into main Apr 9, 2025
1 check passed
@micbar micbar deleted the dev-docs branch April 9, 2025 14:31
@micbar micbar added Type:Maintenance E.g. technical debt, packaging, etc. Docs:Build&Tools labels Apr 9, 2025
@openclouders openclouders mentioned this pull request Apr 10, 2025
Merged
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

@AlexAndBear AlexAndBear AlexAndBear approved these changes

Assignees

No one assigned

Labels

Docs:Build&Tools Type:Maintenance E.g. technical debt, packaging, etc.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@micbar @AlexAndBear