agda/test/Compiler/simple/Issue2714.agda

-- Andreas, 2017-08-23, issue #2714

-- Make sure we produce a warning about missing main function
-- even though we import a module with --no-main.

open import Issue2712