David Greenman 75d8591e04 Fixed bug where vnode_pager_uncache() wasn't always called when it should
be. The result was that the file's space wouldn't be properly freed when
it was deleted.

Submitted by:	John Dyson
1995-08-06 11:55:25 +00:00
..