| commit | 992aeed80b0a6ef1d60ce01df52f3397c3274f35 | [log] [tgz] |
|---|---|---|
| author | Tom Tromey <tromey@adacore.com> | Thu Aug 11 10:07:18 2022 -0600 |
| committer | Tom Tromey <tromey@adacore.com> | Wed Aug 31 11:03:39 2022 -0600 |
| tree | 1a7af982504b79000f29ccf44ef52e739b7e1a97 | |
| parent | 55a6603404099c0b61a5e4613712d3935c2e2bb6 [diff] |
Use ui_out_redirect_pop in more places This changes ui_out_redirect_pop to also perform the redirection, and then updates several sites to use this, rather than explicit redirects.