Use $decimal in timestamp.exp
authorTom Tromey <tom@tromey.com>
Wed, 28 Dec 2022 17:07:45 +0000 (10:07 -0700)
committerTom Tromey <tom@tromey.com>
Wed, 28 Dec 2022 17:07:45 +0000 (10:07 -0700)
commit0a923a6adb9b5a69f03ecd899a0e04881ee5364c
treea98c72c3de0155ca7f04906c3e1bbd64dc50d688
parenta60535c39ba52d88c47740db6ab116db32e2331a
Use $decimal in timestamp.exp

This patch fixes a review comment by Tom de Vries.  He pointed out
that the new timestamp.exp should use the $decimal convenience regexp.
gdb/testsuite/gdb.base/timestamp.exp