Oops, undo previous change, which wasn't supposed to escape from my

machine. Luckily everyone is asleep, so I didn't have to use the time
machine.