GitLab

(Info-fontify-node, Info-bookmark-make-record): Remove the
file extension from Info-current-file.

Fixes: debbugs:13016