fixeria submitted this change.

View Change

contrib/jenkins_manuals: fix doc/manuals paths

Change-Id: Ibfccefec7e44a4803d4ff8ad061db395fc498b89
---
M contrib/jenkins_manuals.sh
1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/jenkins_manuals.sh b/contrib/jenkins_manuals.sh
index 05d53dc..0797f0d 100755
--- a/contrib/jenkins_manuals.sh
+++ b/contrib/jenkins_manuals.sh
@@ -1,7 +1,7 @@
 #!/bin/sh -ex
 
-make -C docs/manuals
+make -C doc/manuals
 
 if [ "$PUBLISH" = "1" ]; then
-	make -C docs/manuals publish
+	make -C doc/manuals publish
 fi

To view, visit change 42452. To unsubscribe, or for help writing mail filters, visit settings.