diff configure @ 710:3e930ea94db6

Rename time-frequency box to plain box - but also reload sessions if they have the "old" name (even though it was only used in 4.0-pre1 exports)
author Chris Cannam
date Wed, 25 Sep 2019 09:52:30 +0100
parents f7ec9e410108
children
line wrap: on
line diff