-- Andreas, 2017-05-17, issue #2574 reported by G. Allais

open import Issue2574Import        -- The imported module should be clickable.
open import Issue2574ImportBlank   -- The imported module should be clickable.
