mirror of https://github.com/OpenIdentityPlatform/OpenDJ.git
parent: 9e25366b | patch | commit | ignore whitespace
Mark Craig
30.07.2015 00de66c59fc4c113eea617cc7deecaddeecba062 
Improve comment
1 files modified
6 ■■■■■ changed files
opendj-server-legacy/pom.xml 6 ●●●●● patch | view | raw | blame | history 
 opendj-server-legacy/pom.xml


@@ -1902,7 +1902,11 @@


    </profile>




    <profile>


      <!-- Build documentation -->


      <!--


        Build the configuration reference, reference documentation source files,


        and assemble artifacts from the results.


        The artifacts are used when preparing the product documentation.


      -->


      <id>docs</id>




      <build>