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

integrate idris-mode and idris2-mode #539

Open
ywata opened this issue Jul 28, 2021 · 0 comments
Open

integrate idris-mode and idris2-mode #539

ywata opened this issue Jul 28, 2021 · 0 comments

Comments

@ywata
Copy link
Contributor

ywata commented Jul 28, 2021

As I tried idris-mode and idris2-mode, I did not understand the difference. So, I changed idris2- etc into idris-, and manual modification to minimize the difference. I found, there are not so much difference between the two. If it is possible, I'd like to propose to merge back to idris2-mode into idris-mode to reduce maintenance efforts.

Actually, I'm not fully understand the detail but I analyzed the difference. The updated branches are in my repository.
https://github.com/ywata/idris-mode idris-mode-working and idris2-mode-working
diff.txt

I marked DECISION N to indicate items we need to decide and NEED INVESTIGATION to mark which I'm not sure about at this moment.
The diffs are from my repository https://github.com/ywata/idris-mode diff between idris-mode-working and idris2-mode-working. They are normalized to make diff minimal.

Could you take a look at the diff?

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

No branches or pull requests

1 participant