Skip to content

fix forgotten rename: head_redex -> base_redex

Ralf Jung requested to merge ralf/base_redex into master

This was missed in !1012 (merged).

Merge request reports