Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Add Android Export feature #545
Hi Venkat. Thanks for the pull request. I have some concerns about the performance implications of this change, and there are some critical times coming up (CodeWorld is being used for an ICFP presentation in a few hours, and at Chalmers through this coming Tuesday. Since this adds the possibility of an expensive server-side build process, it's best not to merge this until after those milestones have passed. I'll take a look soon, though, and see if there are any major concerns.