diff options
Diffstat (limited to 'docs/fr/Makefile')
| -rw-r--r-- | docs/fr/Makefile | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/docs/fr/Makefile b/docs/fr/Makefile index 24ff3e64e..cf7d5af04 100644 --- a/docs/fr/Makefile +++ b/docs/fr/Makefile @@ -41,13 +41,13 @@ dot: filename=$$(basename -- "$$FILE") ; \ extension="$${filename##*.}" ; \ filename="$${filename%.*}" ; \ - echo $$extension ; \ - echo $$filename ; \ - dot -Tpng source/media-src/$$filename.dot > \ - source/_static/$$filename.png ; \ + dot -Tsvg source/media-src/$$filename.dot > \ + source/media-src/$$filename.svg ; \ + #dot -Tpng source/media-src/$$filename.dot > \ + # source/_static/$$filename.png ; \ done -html: dot +html: $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html @echo @echo "Build finished. The HTML pages are in $(BUILDDIR)/html." |