pin¶
Warning
Dune Package Management is not final yet and the configuration options are subject to change.
Pins are package overrides used in the context of package management. They allow to fix a package at a specific version which is not affected by the package repositories selected.
- (pin ...)
Added in version 3.14.
Define a package override.
- (url <string>)
The URL of the package source.
This can be a path to a directory on the local file system or remote Git repository. Local paths can be absolute or relative, and may optionally begin with
file://
though this is not necessary. Remote Git repository URLs must begin withgit+
, for examplegit+https://github.com/user/repo
orgit+git@github.com:user/repo.git
.This must be specified.
- (package ...)
Defines which package is to be pinned.
This must be specified.
- (name <string>)
The name of the package.
This must be specified.
- (version <string>)
The version that the package should be assumed to be. Defaults to
dev
if unspecified.
See also
pin stanza in dune-workspace for workspace-wide pinning.