Option for int gps time
Would like an option for the given GPS time to be an integer. This would help with ndscope compatibility, in particular when copy/pasting into the GPS text entry boxes (though ndscope should be able to handle GPS decimals).
Perhaps the default GPS output could be an integer, and a "verbose" flag could be for decimals. This makes more sense to me since most people are not asking for decimal precision on GPS time from the command line.