Minor fixes.

5 jobs for v0.7.2 in 14 minutes and 10 seconds (queued for 1 second)
Status Name Job ID Coverage
  Build
passed build #996888

00:05:10

passed buildgui #996889

00:03:56

 
  Test
passed linting #996890

00:01:57

passed tests #996891

00:08:13

76.0%
 
  Release
passed release #996892
manual

00:00:46