I installed the attached, which should fix the bug, and also improve display of 
integers while we're in the neighborhood.