one more index for pg_tablespace?

hello ...

i have come an interesting corner case this morning and i am not sure
if it is worth treating this as a bug or as just "bad luck".
imagine creating a directory along with a tablespace ...
hans-jurgen-schonigs-macbook:html hs$ mkdir /tmp/x
hans-jurgen-schonigs-macbook:html hs$ psql test
psql (8.4.1)
Type "help" for help.

test=# create tablespace x location '/tmp/x';
CREATE TABLESPACE
test=# create tablespace x2 location '/tmp/x';
ERROR:  directory "/tmp/x" is not empty
test=# \q

postgres errors our here correctly because it sees that the tablespace
is not empty. this is perfect ...

hans-jurgen-schonigs-macbook:html hs$ cd /tmp/x
hans-jurgen-schonigs-macbook:x hs$ ls
PG_VERSION
hans-jurgen-schonigs-macbook:x hs$ rm PG_VERSION

now, after killing the PG_VERSION file, i am able to create a
tablespace pointing to the same directoy.
this should be prevented by one more unique index on the directory.

hans-jurgen-schonigs-macbook:x hs$ psql test
psql (8.4.1)
Type "help" for help.

test=# create tablespace x2 location '/tmp/x';
CREATE TABLESPACE
test=# \d pg_tablespace  Table "pg_catalog.pg_tablespace"   Column    |   Type    | Modifiers
-------------+-----------+----------- spcname     | name      | not null spcowner    | oid       | not null spclocation
|text      | spcacl      | aclitem[] | 
Indexes:    "pg_tablespace_oid_index" UNIQUE, btree (oid), tablespace
"pg_global"    "pg_tablespace_spcname_index" UNIQUE, btree (spcname), tablespace
"pg_global"
Tablespace: "pg_global"

test=# SELECT * FROM pg_tablespace;  spcname   | spcowner |  spclocation  | spcacl
------------+----------+---------------+-------- pg_default |       10 |               | pg_global  |       10 |
      | x          |       10 | /tmp/x        | x2         |       10 | /tmp/x        | 
(6 rows)

now, killing PG_VERSION manually is not what people do but what can
happen is that, say, an NFS connection is gone or that somehow the
directory is empty because of some other network filesystem doing some
funny thing. it is quite realistic that this can happen.

how about one more unique index here?
pg_tablespace does not look too good with a duplicate entry ...
many thanks,
    hans


--
Cybertec Schönig & Schönig GmbH
Reyergasse 9 / 2
A-2700 Wiener Neustadt
Web: www.postgresql-support.de