-
Notifications
You must be signed in to change notification settings - Fork 1k
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
chore(Dev): ignore .idea directory that Intellij IDEs add automatically #1903
Conversation
I do not think this kind of configs should be managed at this project. User specific development setting including editor config should be set in global config. See also the discussion at #620 (comment). |
I theoretically agree that would be better, but the cost of having this seems extremely low. |
Are you of the opinion that even things that should not really be managed are managed because the cost is low? |
Globally ignoring the .idea folder is not workable for many as IntelliJ recommends that you commit the directory in order to share configuration with colleagues. |
You can just add it explicitly in those projects. |
|
The fact that
I think it's a basic thought not to manage developer-specific settings in projects. There's no particular reason to treat JetBrains tools as special, and the same can be said for all tools. This principle should be followed unless there is a special reason, and I do not think this is an exceptional case. Moreover most of the tokio and hyper projects to which tonic belongs do not use project's
I opened the pull request because I felt that you showed some understanding by #1903 (comment). The pull request is something I believe will improve the project. I'm surprised you made such a claim. You merged this pull request, which contains issues, without giving people enough time to comment and discussion. Unlike you, I did not without giving time for discussion. If you are of the opinion that complete discussion and agreement are necessary to do anything, then shouldn't you first revert this pull request that was merged without discussion and agreement. |
I agree there's no particular reason to treat JetBrains tools as special, and I'd be happy to merge similar PRs for other tools. In projects that I (help) maintain it is common to ignore these.
That's a surprising interpretation to me, but okay.
I merged it as a maintainer -- the submitter proposed it and it made sense to me. Since I've been similar PRs across many projects that have usually been merged, I saw no reason to consider this controversial. Given the extremely limited impact and zero risk from this PR, I think merging without waiting for discussion makes sense in that scenario. I don't think it makes sense to change the status quo (that is, with the PR merged) until this discussion has run its course. |
My position as a maintainer is that this repository should not manage configuration that depends on a user's specific environment. These settings should be configured by the user using the appropriate way provided for them, and the project should not assume the user's responsibility for configuring them with inappropriate way. |
#1907, which fixes this, has been merged since there were no additional objections or discussions. |
I find it very offputting that you merged #1907 while this discussion is unresolved. |
I'm surprised to hear you say that, since you merged this pull request without leaving any time for discussion. It is legitimate to revert it first and then discuss the necessity. You have merged without consensus before and are continuing to do so now. I don't do that, but I won't condone it again and again. This time, I prepared a lot longer to discuss it than when you had merged this immediately, but you said that we should leave it as it is during the discussion, but you remained silent and did not move the discussion forward. This is very unpleasant and I feel it is an arbitrary way. I will deal with attitudes that try to leave this without any discussion. As a result, the discussion was ended, so this has been fixed. Please note that there are times when we judge that discussion is unnecessary and merge, but it is only appropriate when that judgment is correct, and if it is not, the merged state will not be valid. So it makes sense to discuss whether it is appropriate to add it, not discussing revert this back. That's where the right discussion begins. |
This is the stance that I stand by generally.
I did not know they suggested this but I think its also possible to commit files that are also ignored. So setting a global ignore and committing .idea files for your colleagues shouldn't be mutually exclusive. My stance on this in general is that we shouldn't merge things like @djc @tottoto I think merging things and even something like this quickly if you think its okay is fine, it is really a small change that doesn't affect the library and I would encourage both of you if you feel like there is something like this that you want to get merged go for it. Of course think about how it will affect things. There will always be an issue of timezones and general availability making it hard for others to chime in a timely manner hence @tottoto missing the initial merge. In this case, I would have rather that at least one of you have pinged me about this disagreement (both of you could have done this!) and that we could resolve things a bit earlier in the process without it reaching this sort of stage. I would like to be the final authority on reverting and/or merging things that may be contentious. I really appreciate both of you for helping out with the project. I am generally very easy to reach on discord or via email if you have any questions please do reach out. EDIT: Removed some unfair criticism of tottoto. |
Very minor quality-of-life thing; I keep accidentally committing the dir that IDEA creates and having to remove it.