GitLab

(compilation--previous-directory): New fun.
(compilation--previous-directory-cache): New var.
(compilation--remove-properties): Flush it.
(compilation-directory-properties, compilation-error-properties):
Use the new fun to speed up looking for the current directory.