Skip to content

Fix --debug flag#593

Merged
jcp19 merged 3 commits intomasterfrom
joao-improve-debug-mode
Jan 12, 2023
Merged

Fix --debug flag#593
jcp19 merged 3 commits intomasterfrom
joao-improve-debug-mode

Conversation

@jcp19
Copy link
Contributor

@jcp19 jcp19 commented Jan 6, 2023

Currently, --debug leads to crashes due to how FileWriterReporter is implemented: when the input source in the reported message is /builtin/builtin.gobra, it tries to generate a file /builtin/builtin.gobra.XXX (where XXX can be an extension like internal, or vpr) for which a regular typically does not have permission.

Additionally, I made some changes for the debug mode to produce less output, otherwise it is pretty much useless

@jcp19 jcp19 requested a review from Dspil January 6, 2023 19:58
@jcp19 jcp19 merged commit c11000d into master Jan 12, 2023
@jcp19 jcp19 deleted the joao-improve-debug-mode branch January 12, 2023 10:44
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.

2 participants