Rewrite local opam repository into a different folder and .gitignore it
This commit is contained in:
parent
834cc8c072
commit
8821e6c01e
@ -37,7 +37,7 @@ before_script:
|
|||||||
local-dune-job:
|
local-dune-job:
|
||||||
script:
|
script:
|
||||||
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
||||||
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository/"
|
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local/"
|
||||||
- opam install -y --build-test --deps-only ./src/
|
- opam install -y --build-test --deps-only ./src/
|
||||||
- (dune build -p ligo)
|
- (dune build -p ligo)
|
||||||
# TODO: also try instead from time to time:
|
# TODO: also try instead from time to time:
|
||||||
@ -47,7 +47,7 @@ local-dune-job:
|
|||||||
local-repo-job:
|
local-repo-job:
|
||||||
script:
|
script:
|
||||||
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
||||||
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository/"
|
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local/"
|
||||||
#--build-test
|
#--build-test
|
||||||
- opam install -y ligo
|
- opam install -y ligo
|
||||||
|
|
||||||
|
1
vendors/.gitignore
vendored
Normal file
1
vendors/.gitignore
vendored
Normal file
@ -0,0 +1 @@
|
|||||||
|
/ligo-opam-repository-local
|
2
vendors/ligo-opam-repository
vendored
2
vendors/ligo-opam-repository
vendored
@ -1 +1 @@
|
|||||||
Subproject commit c794c6169960fd6d625ec2eb292f4136ec276f99
|
Subproject commit 2b4eaa29d1c4066ddaba047216e27719ea737581
|
Loading…
Reference in New Issue
Block a user