diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.global.in | 4 | ||||
| -rw-r--r-- | src/include/Makefile | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/src/Makefile.global.in b/src/Makefile.global.in index 2eff4d4067f..69512ac6437 100644 --- a/src/Makefile.global.in +++ b/src/Makefile.global.in @@ -18,9 +18,9 @@ # # Meta configuration -standard_targets = all install installdirs uninstall distprep clean distclean maintainer-clean coverage check installcheck +standard_targets = all install installdirs uninstall distprep clean distclean maintainer-clean coverage check installcheck maintainer-check -.PHONY: $(standard_targets) install-strip maintainer-check html man installcheck-parallel +.PHONY: $(standard_targets) install-strip html man installcheck-parallel # make `all' the default target all: diff --git a/src/include/Makefile b/src/include/Makefile index 0d5f04932b5..1bfb4a7166d 100644 --- a/src/include/Makefile +++ b/src/include/Makefile @@ -67,3 +67,6 @@ clean: distclean maintainer-clean: clean rm -f pg_config.h dynloader.h pg_config_os.h stamp-h + +maintainer-check: + cd catalog && ./duplicate_oids |