+if (@$_SERVER['PATH_INFO']) {
+ $file = $_SERVER['PATH_INFO'];
+ // If it ends with a slash it's a directory so we add index.xbf.
+ if (substr($_SERVER['PATH_INFO'], strlen($_SERVER['PATH_INFO'])-1) == '/') {
+ $file .= 'index.xbf';
+ }
+} else {
+ $file = 'index.xbf';
+}