* New data

[helm.git] / helm / mowgli / home / html / Makefile

diff --git a/helm/mowgli/home/html/Makefile b/helm/mowgli/home/html/Makefile
index 304c75d31af017463bf9553dff60cf6b6a8390c2..1455b47d930ed1ad933d4d803cf26de5c6fbe3bc 100644 (file)
--- a/helm/mowgli/home/html/Makefile
+++ b/helm/mowgli/home/html/Makefile
@@ -45,6 +45,7 @@ PEOPLE = \
                people/inria/pottier.html \
                people/inria/rideau.html \
                people/inria/thery.html \
+               people/inria/werner.html \
                people/nijmegen/barendregt.html \
                people/nijmegen/barreiro.html \
                people/nijmegen/cohen.html \
@@ -54,7 +55,8 @@ PEOPLE = \
                people/nijmegen/stein.html \
                people/nijmegen/synek.html \
                people/nijmegen/wiedijk.html \
-               people/trusted-logic/bolignano.html
+               people/trusted-logic/bolignano.html \
+               people/trusted-logic/gimenez.html
 
 DOCUMENTS = \
             index.html \