Your reasoning is valid and the fix is correct. I've made a corresponding change.
Thanks.
You can still improve, though, by sending in a git patch next time. In addition to making it even more convenient for us, such a transaction will create a record on our blockchain (called git) for others to see and earn you reputation. 😄
Will do next time! Bye, Johannes _______________________________________________ bug-auctex mailing list [email protected] https://lists.gnu.org/mailman/listinfo/bug-auctex
