Skip to content

Commit

Permalink
pyk RPC: bug-report w/o dt dir (#4340)
Browse files Browse the repository at this point in the history
The `llvm_definition/dt` directory in the bug report is not necessary
(any more), and is usually very big.
Closes runtimeverification/kasmer-multiversx#98

---------

Co-authored-by: rv-jenkins <[email protected]>
  • Loading branch information
jberthold and rv-jenkins authored May 14, 2024
1 parent f87c271 commit 0e2f39d
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion pyk/src/pyk/kore/rpc.py
Original file line number Diff line number Diff line change
Expand Up @@ -1354,7 +1354,6 @@ def _extra_args(self) -> list[str]:
def _populate_bug_report(self, bug_report: BugReport) -> None:
super()._populate_bug_report(bug_report)
bug_report.add_file(self._llvm_definition, Path('llvm_definition/definition.kore'))
bug_report.add_file(self._llvm_dt, Path('llvm_definition/dt'))
llvm_version = run_process('llvm-backend-version', pipe_stderr=True, logger=_LOGGER).stdout.strip()
bug_report.add_file_contents(llvm_version, Path('llvm_version.txt'))

Expand Down

0 comments on commit 0e2f39d

Please sign in to comment.