Skip to content
Snippets Groups Projects
Commit 6a0896a2 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/deprecate_rev_length' into 'master' 

Unsilence deprecation warning regarding list lemmas.

See merge request !574
parents d297a432 2db35c48
Pipeline #106988 passed
Stage: build