>
Large unneeded files can be deleted with "rm".
This is what I ended up doing. The version 25 was in currently use and I rm'ed all the old version files.
That worked, but I needed to do the same when version 31 appeared. Fortunately the new version will get into use so rm will work.
Maybe apt-get upgrade could use some magic to get around the space limitation issue. Or maybe something else could be done.
At install time it would be good to suggest some good size for the boot partition. I did search a bit but ended up creating a too small partition, maybe the info was too old.
Thanks all!