mirror of
https://github.com/chshersh/github-tui.git
synced 2024-10-05 14:57:53 +03:00
Specify pin depends
This commit is contained in:
parent
7d4a4f302e
commit
7a6547888a
@ -33,3 +33,6 @@ build: [
|
||||
]
|
||||
]
|
||||
dev-repo: "git+https://github.com/chshersh/github-tui.git"
|
||||
pin-depends: [
|
||||
["minttea.dev" "git+https://github.com/leostera/minttea"]
|
||||
]
|
||||
|
3
github_tui.opam.template
Normal file
3
github_tui.opam.template
Normal file
@ -0,0 +1,3 @@
|
||||
pin-depends: [
|
||||
["minttea.dev" "git+https://github.com/leostera/minttea"]
|
||||
]
|
Loading…
Reference in New Issue
Block a user