From 7a7f0009af7ee37ab34655774215da2bf325c6bd Mon Sep 17 00:00:00 2001 From: Slava Pestov Date: Sun, 29 Jun 2008 02:17:46 -0500 Subject: [PATCH] Remove obsolete deploy descriptor --- extra/factory/deploy.factor | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 extra/factory/deploy.factor diff --git a/extra/factory/deploy.factor b/extra/factory/deploy.factor deleted file mode 100644 index 84dd43b7e1..0000000000 --- a/extra/factory/deploy.factor +++ /dev/null @@ -1,12 +0,0 @@ -USING: tools.deploy.config ; -V{ - { strip-globals? f } - { strip-word-props? f } - { strip-word-names? f } - { strip-dictionary? f } - { strip-debugger? f } - { deploy-math? t } - { deploy-compiled? t } - { deploy-io? f } - { deploy-ui? f } -}