X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/1c246434aa207f53d878f29b596b1d9519680c2f..3f07a40e5a17c2bce4d90e1a154f8a73d476aaaa:/Makefile diff --git a/Makefile b/Makefile index f32d0b0..4cbd293 100644 --- a/Makefile +++ b/Makefile @@ -85,7 +85,8 @@ bin/domtool-client: openssl/mlton/FFI/libssl.h.mlb \ bin/domtool-slave: openssl/mlton/FFI/libssl.h.mlb \ src/domtool-slave.mlb src/domtool.lex.sml \ src/domtool.grm.sig src/domtool.grm.sml \ - $(COMMON_DEPS) src/*.sig src/*.sml + $(COMMON_DEPS) src/*.sig src/*.sml \ + src/plugins/*.sig src/plugins/*.sml mlton -output bin/domtool-slave -link-opt -ldl src/domtool-slave.mlb install: @@ -94,3 +95,8 @@ install: cp bin/domtool-server /usr/local/sbin/ cp bin/domtool-slave /usr/local/sbin/ cp bin/domtool-client /usr/local/bin/domtool + +.PHONY: grab_lib + +grab_lib: + rsync --delete /afs/hcoop.net/common/etc/domtool/lib/* lib/