diff options
Diffstat (limited to 'gnattools/Makefile.in')
| -rw-r--r-- | gnattools/Makefile.in | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/gnattools/Makefile.in b/gnattools/Makefile.in index 3a1a0544271..3bfa04f1d06 100644 --- a/gnattools/Makefile.in +++ b/gnattools/Makefile.in @@ -302,6 +302,9 @@ info: # Build DVI (none here). dvi: +# Build HTML (none here). +html: + # Build TAGS (none here). TAGS: @@ -310,6 +313,8 @@ install: install-info: +install-html: + # Cleaning rules. mostlyclean: |