diff options
| author |  Benjamin Jones <bjones@galois.com> | 2012-10-23 11:42:28 -0700 |
|---|---|---|
| committer | Benjamin Jones <bjones@galois.com> | 2012-10-23 11:42:28 -0700 |
| commit | 658da03955fd69a2eb9d33972a832877f3fcbf56 (patch) | |
| tree | f1fa6d2715cdd1aec56f80acae6850ba8139d3e3 /doc | |
| parent | 365412727345ab3619958e120bab982fddcdf9e7 (diff) | |
| parent | 904c26f350a44e4906cf0a25cd363930047cf897 (diff) | |
Merge branch 'wip'
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile index fb2fecb..e9539c1 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -5,8 +5,8 @@ MAN_DEPS=$(MANUAL_SRC)/*.md $(MANUAL_SRC)/figures/*.png jsdoc-toolkit=../build/jsdoc -jsdoc: ../contexts/data/fiveui/injected/prelude.js - @$(jsdoc-toolkit) ../contexts/data/fiveui/injected/prelude.js +jsdoc: ../contexts/data/fiveui/injected/prelude.js ../contexts/data/fiveui/injected/jquery-plugins.js + @$(jsdoc-toolkit) ../contexts/data/fiveui/injected/prelude.js ../contexts/data/fiveui/injected/jquery-plugins.js .PHONY: man man: web-manual |