-
Robbert Krebbers authored
We only use wp_value in the end if the resulting goal is yet another wp. Otherwise we may not be able to do a final view shift (as observed by Ralf).
cd509c3f
We only use wp_value in the end if the resulting goal is yet another wp. Otherwise we may not be able to do a final view shift (as observed by Ralf).