diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/releases/default.nix | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/releases/default.nix b/tools/releases/default.nix index d38ca0b5d8be..aedf396aeef1 100644 --- a/tools/releases/default.nix +++ b/tools/releases/default.nix @@ -19,8 +19,8 @@ in set -e export PATH="${makeBinPath [ pkgs.git depot.third_party.josh ]}:$PATH" - echo 'Filtering depot through ${filter}' - josh-filter '${filter}' + echo 'Filtering depot through :unsign ${filter}' + josh-filter ':unsign ${filter}' echo 'Fetching remote to check if a push is needed' git fetch '${remote}' '${ref}' |