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

🔧 Configure online editor. #234

Closed
wants to merge 1 commit into from

Conversation

BramVanPevenage
Copy link
Contributor

associated issue #142

used style guide

modified indentation to 2

Copy link
Contributor

@rainij rainij left a comment

Choose a reason for hiding this comment

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

I looked into the history of config.json. The previous value (4) seems to be randomly set. So if the style guide you mentioned suggests 2 I am fine with that.

@rainij
Copy link
Contributor

rainij commented Jul 14, 2023

@BramVanPevenage sorry for the late feedback, for some reason I got no notification. I just happened to get a notification by another PR. You can merge the PR (hope you are allowed to do it).

@BramVanPevenage
Copy link
Contributor Author

@rainij no problem, it will automatically merge after the required statuses and checks are done.

@BNAndras
Copy link
Member

@BramVanPevenage It seems like the configlet CI check is stuck so the auto merge didn't happen through as expected.

@rainij
Copy link
Contributor

rainij commented Oct 31, 2023

@BramVanPevenage maybe you can rebase this to trigger a new run of the configlet CI. Would be nice to merge this.

@BramVanPevenage BramVanPevenage changed the title 🔧 Configure online editor 🔧 Configure online editor. Nov 11, 2023
@BramVanPevenage
Copy link
Contributor Author

check #243

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.

3 participants