PublicWithoutOpen.agda:5,14-20
Keyword 'public' is ignored here
when scope checking the declaration
  module B = A public

———— All done; warnings encountered ————————————————————————

PublicWithoutOpen.agda:5,14-20
Keyword 'public' is ignored here
when scope checking the declaration
  module B = A public
