From 7c93d58e4fec42f1f90b7b6a425f7c9c50425bac Mon Sep 17 00:00:00 2001 From: Michael Jastram <michael@jastram.de> Date: Wed, 25 Jan 2012 14:46:14 +0000 Subject: [PATCH] One more fix to index-script git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@14051 1434b563-b632-4741-aa49-43a3a8374d2e --- org.rodinp.handbook.feature/customBuild.xml | 2 +- org.rodinp.handbook.feature/latex/.creative-commons.tex.ini | 3 +++ .../org.rodinp.handbook.feature customBuild.xml.launch | 1 + org.rodinp.handbook.feature/test.txt | 1 - 4 files changed, 5 insertions(+), 2 deletions(-) create mode 100644 org.rodinp.handbook.feature/latex/.creative-commons.tex.ini delete mode 100644 org.rodinp.handbook.feature/test.txt diff --git a/org.rodinp.handbook.feature/customBuild.xml b/org.rodinp.handbook.feature/customBuild.xml index 14d8f56..3bab3ee 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 0000000..3038328 --- /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 0943538..f121b17 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 8bebc6c..0000000 --- a/org.rodinp.handbook.feature/test.txt +++ /dev/null @@ -1 +0,0 @@ -hallo world -- GitLab