diff options
author | jim winstead <jimw@php.net> | 2002-03-16 00:21:40 +0000 |
---|---|---|
committer | jim winstead <jimw@php.net> | 2002-03-16 00:21:40 +0000 |
commit | d3400b2b5f065c9fcef9d655afd4c1c81e7a2c18 (patch) | |
tree | 4c00c9a5f1a44410a157bb48ec0c602a28775c14 /ext/ovrimos | |
parent | 8dfe4961c46afa827679d12ed3339c797c86f3f3 (diff) | |
download | php-git-d3400b2b5f065c9fcef9d655afd4c1c81e7a2c18.tar.gz |
the 'setup' script was removed more than two years ago.
these can be safely removed from the 4.2 branch, too.
Diffstat (limited to 'ext/ovrimos')
-rw-r--r-- | ext/ovrimos/setup.stub | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/ext/ovrimos/setup.stub b/ext/ovrimos/setup.stub deleted file mode 100644 index 5e7778e9be..0000000000 --- a/ext/ovrimos/setup.stub +++ /dev/null @@ -1,6 +0,0 @@ -# $Source$ -# $Id$ - -define_option with-ovrimos 'ovrimos support?' yesnodir no \ -' Whether to build the ovrimos extension.' - |