diff options
| author | Julian Andres Klode <jak@debian.org> | 2019-02-04 12:44:08 +0000 |
|---|---|---|
| committer | Julian Andres Klode <jak@debian.org> | 2019-02-04 12:44:08 +0000 |
| commit | 3a015964dd56edf897ee062b2eafa2cfc0584380 (patch) | |
| tree | b7c47f960d6281195ea7fd3f90a6404b939df134 /cmdline | |
| parent | d5dcc2e9d3008b57c3fae0bcb5b1c2a197f5430c (diff) | |
| parent | c2b9b0489538fed4770515bd8853a960b13a2618 (diff) | |
Merge branch 'pu/dead-pin' into 'master'
A pin of -32768 overrides any other, disables repo
See merge request apt-team/apt!40
Diffstat (limited to 'cmdline')
0 files changed, 0 insertions, 0 deletions