Skip to content

Commit

Permalink
[ fix ] my silly mistake
Browse files Browse the repository at this point in the history
  • Loading branch information
@gallais
gallais committed Apr 16, 2024
1 parent e200afc commit 9ae32c5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/IO/Primitive.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

module IO.Primitive where

open import IO.Primitive public
open import IO.Primitive.Core public

{-# WARNING_ON_IMPORT
"IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."
Expand Down

0 comments on commit 9ae32c5

Please sign in to comment.