Merge pull request #14074 from keszybz/rename-system-options

author Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>

Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)

committer GitHub <noreply@github.com>

Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)
author Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)
committer GitHub <noreply@github.com>
Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)
diff --cc NEWS
Simple merge
diff --cc src/core/path.c
Simple merge
author	Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
	Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)
committer	GitHub <noreply@github.com>
	Wed, 20 Nov 2019 15:13:46 +0000 (16:13 +0100)
		1	2
NEWS	patch \|	diff1 \|	diff2 \|	blob \| history
src/core/path.c	patch \|	diff1 \|	diff2 \|	blob \| history