joerg eb2a50b7f8 Install a script as script, so it doesn't get stripped.		2020-08-11 18:40:45 +00:00
..
patch-Makefile	Install a script as script, so it doesn't get stripped.	2020-08-11 18:40:45 +00:00