Skip to content

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