Version 4.0 Patchlevel 5 Added Features/Bug Fixes

1. Fix a bug that generates bad a GIF file when running tgif with "-print -gif" commandline arguments. Thanks to Dick Wesseling <ftu@fi.uu.nl> for pointing out this problem.

2. Support more tgif file name extensions. Allow ".tgo" to also be a tgif object file name extension and ".tgs" to also be a tgif symbol file name extension.