Skip to content

Add dotty support #60

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

Closed

Conversation

alexarchambault
Copy link
Collaborator

@alexarchambault alexarchambault commented Nov 26, 2018

This is a WIP, just opening that to run the CI…

@alexarchambault alexarchambault mentioned this pull request Nov 27, 2018
@alexarchambault alexarchambault force-pushed the topic/dotty branch 2 times, most recently from 723ac72 to 3f915ca Compare November 27, 2018 10:31
@alexarchambault alexarchambault changed the title Add dotty support (WIP) Add dotty support Nov 27, 2018
@alexarchambault
Copy link
Collaborator Author

Thinking about pushing this in a branch named dotty in this repo… Everyone's ok with that? (@lihaoyi? @olafurpg?)

@alexarchambault
Copy link
Collaborator Author

Then adding sourcecode to the dotty community build.

@lihaoyi
Copy link
Member

lihaoyi commented Nov 27, 2018 via email

@alexarchambault
Copy link
Collaborator Author

@lihaoyi I guess the dotty team will make sure the dotty macro support doesn't break sourcecode in the future, thanks to that. (Or at least, they'll be aware of it if they do…)

@alexarchambault
Copy link
Collaborator Author

Done, pushed as a branch named dotty.

@alexarchambault alexarchambault deleted the topic/dotty branch November 27, 2018 11:30
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