[mapserver-dev] Pull requests in documentation

[Jeff McKenna]

Hi ThomasG,

Actually I solved it by commenting out the test lines in the
build_docs.sh temporarily, then ran the script manually, and it all
worked on the visible site.  (as you see now)

Let me know if you notice any problems again on the server.

Thanks for this great contribution!

-jeff



On 2013-12-09 6:15 PM, Thomas Gratier wrote:
> Hi,
> 
> Trying the same thing on my branch, I also had the problem.
> I solved it by adding an unnecessarycommit (like a new line in Makefile)
> using Github GUI.
> So pushing any correction on a file in the branch-6-4 will normally
> solve the deploy problem.
> Be careful, on mapserver.org <http://mapserver.org> website, everything
> seems to work (French entry is alright http://mapserver.org/fr/ now) so
> no need to use this dirty trick.
> 
> Cheers
> 
> ThomasG