Alessio Treglia a8a455a6f7 Makefiles: various improvements (#6101) ... Don't reinstall proto tools unconditionally every time one runs make. On most Linux systems, /usr/local is writable by root only. Allow users to customise installation directory by passing PREFIX to make command line, e.g.: $ make PREFIX=~/.local		2020-04-30 21:30:30 +02:00
..
Makefile	Makefiles: various improvements (#6101)	2020-04-30 21:30:30 +02:00