Skip to content

Add ability to select printer #2816

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
Closed
felixmulder opened this issue Jun 27, 2017 · 2 comments
Closed

Add ability to select printer #2816

felixmulder opened this issue Jun 27, 2017 · 2 comments

Comments

@felixmulder
Copy link
Contributor

felixmulder commented Jun 27, 2017 •
edited
Loading

Need to be able to select between:

  • power printer
  • user printer
  • refined printer

Currently the user can see types like SkolemType etc, this is confusing and not very helpful. We still want to keep this for development purposes - but the user facing one needs to be properly implemented.
@felixmulder felixmulder added this to the 0.2 Tech Preview milestone Jun 27, 2017
@felixmulder felixmulder changed the title Being able to select printer Add ability to select printer Jun 27, 2017
@smarter
Copy link
Member

smarter commented Jul 6, 2017

I added a -Yprint-debug option in #2835 for this purpose, doesn't do much yet.

@smarter smarter modified the milestones: 0.3 Tech Preview, 0.2 Tech Preview Jul 11, 2017
@allanrenucci allanrenucci removed this from the 0.5 Tech Preview milestone Nov 30, 2017
@smarter
Copy link
Member

smarter commented Jan 26, 2019 •
edited
Loading

Closing given the previous comment, separate issues should be open if we see something weird being printed in error messages etc.

@smarter smarter closed this as completed Jan 26, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@smarter @felixmulder @allanrenucci