More work on bug #8378.  The export now works.