diff options
-rw-r--r-- | build/VERSION.properties | 1 | ||||
-rw-r--r-- | build/build.xml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/build/VERSION.properties b/build/VERSION.properties index ecd654e0e1..8c5f8a41fb 100644 --- a/build/VERSION.properties +++ b/build/VERSION.properties @@ -1 +1,2 @@ version=6.4.8 +manual.repository=http://dev.vaadin.com/svn/doc/branches/6.4 diff --git a/build/build.xml b/build/build.xml index f3beda09d5..6fe1f8082d 100644 --- a/build/build.xml +++ b/build/build.xml @@ -881,7 +881,7 @@ <!-- Checkout doc repository. --> <target name="manual-checkout" depends="manual-init" unless="docdir"> - <property name="manual.repository" value="http://dev.vaadin.com/svn/doc/trunk"/> + <!-- The required manual.repository property is defined in VERSION.properties --> <echo>Checking out manual from repository ${manual.repository}</echo> |