diff --git a/org.rodinp.handbook.feature/customBuild.xml b/org.rodinp.handbook.feature/customBuild.xml index 14d8f56cfd2bf2a737376a3aac4493f61be490fc..3bab3eeaf8558db89a53e83e04195a2345e18b4b 100644 --- a/org.rodinp.handbook.feature/customBuild.xml +++ b/org.rodinp.handbook.feature/customBuild.xml @@ -93,7 +93,7 @@ but such elements exist in the index. We replace them. --> <replaceregexp match="plasTeX.Base.LaTeX.Index.IndexDestination[^>]*" - replace="plasTeX.Base.LaTeX.Index.IndexDestination" + replace="plasTeX.Base.LaTeX.Index.IndexDestination/" flags="g" > <fileset dir="${targetdir}" includes="*.html"/> diff --git a/org.rodinp.handbook.feature/latex/.creative-commons.tex.ini b/org.rodinp.handbook.feature/latex/.creative-commons.tex.ini new file mode 100644 index 0000000000000000000000000000000000000000..3038328756a502f50e18861cf7bb73c9465a0586 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.creative-commons.tex.ini @@ -0,0 +1,3 @@ +[LATEX] +master-filename = rodin-doc.tex + diff --git a/org.rodinp.handbook.feature/org.rodinp.handbook.feature customBuild.xml.launch b/org.rodinp.handbook.feature/org.rodinp.handbook.feature customBuild.xml.launch index 0943538cea995ba72c354f248af9ef3889dcd7ab..f121b17cb5df28195382dd7e7700a757faec0daa 100644 --- a/org.rodinp.handbook.feature/org.rodinp.handbook.feature customBuild.xml.launch +++ b/org.rodinp.handbook.feature/org.rodinp.handbook.feature customBuild.xml.launch @@ -15,6 +15,7 @@ <stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.ant.internal.launching.remote.InternalAntRunner"/> <stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="org.rodinp.handbook.feature"/> <stringAttribute key="org.eclipse.jdt.launching.SOURCE_PATH_PROVIDER" value="org.eclipse.ant.ui.AntClasspathProvider"/> +<stringAttribute key="org.eclipse.ui.externaltools.ATTR_ANT_TARGETS" value="generate-eclipse,"/> <stringAttribute key="org.eclipse.ui.externaltools.ATTR_LAUNCH_CONFIGURATION_BUILD_SCOPE" value="${none}"/> <stringAttribute key="org.eclipse.ui.externaltools.ATTR_LOCATION" value="${workspace_loc:/org.rodinp.handbook.feature/customBuild.xml}"/> <stringAttribute key="process_factory_id" value="org.eclipse.ant.ui.remoteAntProcessFactory"/> diff --git a/org.rodinp.handbook.feature/test.txt b/org.rodinp.handbook.feature/test.txt deleted file mode 100644 index 8bebc6cb8897c2e337fab3f4b360d9f510c61d8a..0000000000000000000000000000000000000000 --- a/org.rodinp.handbook.feature/test.txt +++ /dev/null @@ -1 +0,0 @@ -hallo world