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.

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

Print Tables treated as error #806

Open
SkySkimmer opened this issue Jan 16, 2025 · 2 comments
Open

Print Tables treated as error #806

SkySkimmer opened this issue Jan 16, 2025 · 2 comments

Comments

@SkySkimmer
Copy link
Contributor

Run Print Tables., it will treat it like it errored and mangle the output shown in *response*

I guess this is because the output contains Coqtop Exit On Error: off

@hendriktews
Copy link
Collaborator

Thanks for the report, same for Print Options.
Would you know a regular expression that can safely distinguish error messages in coqtop?

@SkySkimmer
Copy link
Contributor Author

Isn't Error: always at the beginning of the line?

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

No branches or pull requests

2 participants