Skip to content

Commit

Permalink
Add note to clean up old file after next release
Browse files Browse the repository at this point in the history
  • Loading branch information
dunhamsteve committed Jul 16, 2023
1 parent 06a6ada commit 914e02e
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Libraries/Utils/Term.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ module Libraries.Utils.Term

%default total

-- TODO: remove this file and use System.Term after version following 0.6.0 is released

libterm : String -> String
libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"

Expand Down

0 comments on commit 914e02e

Please sign in to comment.