-
-
Notifications
You must be signed in to change notification settings - Fork 2.6k
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
Improvements to search #307
Conversation
Can you please remove the |
DONE 😎 |
Sorry for being picky at the formatting. When reading the diff, the indents don't seem to be right. Besides the content of the code, we also want to have the formatting consistent to ease newcomers to read and understand the code. Do you use Eclipse or IntelliJ? With the recent master, |
@koppor I totally agree about the formatting/indenting issues. However, the last time I run the formatter on the files resulted in many formatting changes. Is it possible that you run the formatter on the files after accepting the PR? Otherwise, my commit will be again screwed. |
I will discuss that with the other developers. Meanwhile, I'd like to ask whether you are aware that git gui can do line-based committing: Mark the lines to commit, right click, choose "stage lines to commit". Then, you can collect only the "important" modified lines. I would propose to do the formatting and create a new commit. Amending does not work as your PR already consists of two commits. You could use |
I created a new branch |
Cleaned-up version of #162.