Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: Downgrade wrongly placed doc coment to normal comment
Kani, running using nightly rustc, was warning about this comment. Fix it to resolve the warning during verification, to get slightly cleaner logs. Signed-off-by: Patrick Roy <roypat@amazon.co.uk>
- Loading branch information