diff options
Diffstat (limited to 'databases/pgadmin3/files/patch-Makefile.in')
| -rw-r--r-- | databases/pgadmin3/files/patch-Makefile.in | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/databases/pgadmin3/files/patch-Makefile.in b/databases/pgadmin3/files/patch-Makefile.in new file mode 100644 index 000000000000..b3b5753c7e26 --- /dev/null +++ b/databases/pgadmin3/files/patch-Makefile.in @@ -0,0 +1,11 @@ +--- Makefile.in.orig 2012-11-04 18:15:35.000000000 +0700 ++++ Makefile.in 2012-11-04 18:15:45.000000000 +0700 +@@ -956,7 +956,7 @@ + + # Create HTML docs + doc: +-@SPHINX_BUILD_TRUE@ cd $(top_srcdir)/docs/en_US && make -f Makefile.sphinx SPHINXBUILD=${SPHINX_BUILD} htmlhelp ++@SPHINX_BUILD_TRUE@ cd $(top_srcdir)/docs/en_US && ${MAKE} -f Makefile.sphinx SPHINXBUILD=${SPHINX_BUILD} htmlhelp + + all: doc + |