Commit 98ba9f5f authored by Robbert Krebbers's avatar Robbert Krebbers

Forgot to commit prelude/sorting, this fixes 6dbe0c27.

parent ad5c2676
Pipeline #2360 passed with stage