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.

Sign up for GitHub

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

Jump to bottom

Remove option for indentation #514

Open
chochos opened this issue Mar 27, 2015 · 1 comment
Open

Remove option for indentation #514

chochos opened this issue Mar 27, 2015 · 1 comment
Assignees
@chochos
Labels
optimization
Milestone
1.3

Comments

@chochos
Copy link
Member

chochos commented Mar 27, 2015

I don't think we should even have this option. It's generated code, it's already hard to read because we mangle all the names, I don't see the point in having the option to indent the generated code anymore.
@chochos chochos self-assigned this Mar 27, 2015
chochos added a commit that referenced this issue Apr 6, 2015
@chochos
deprecate and ignore option to indent code #514
1dc4ec5
@chochos chochos added this to the 1.3 milestone May 14, 2015
@chochos
Copy link
Member Author

chochos commented May 14, 2015

I'll leave it deprecated for now.

@CeylonMigrationBot CeylonMigrationBot mentioned this issue Nov 14, 2015
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@chochos chochos

Labels
optimization
Projects
None yet
Milestone
1.3
Development

No branches or pull requests
1 participant
@chochos