Thomas Lange Tue, 26 Dec 2017 04:51:35 -0800
I wonder if we can achieve the same by using apt pinning (man apt_preferences), for e.g. writing a file to /etc/apt/preferences.d/.
-- regards Thomas
