diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 15:44:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 20:22:35 +0200 |
| commit | b7b78d8ca8d6fc6fdb0f744be02c386bc00da8bf (patch) | |
| tree | 9f9c03e501a207c70c7b518f431c744062140ddc /dev | |
| parent | 8b2505b5526395d2ad3c5126624a070e0f55a8af (diff) | |
[loadpath] Further cleanup after merge with MlTop.
We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.
In particular, we remove exceptions in favor a `locate_result` monad.
More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/09895-ejgallego-require+upper.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh new file mode 100644 index 0000000000..9a42c829ce --- /dev/null +++ b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then + + quickchick_CI_REF=require+upper + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi |