Yes, I noticed this as well. They should go, I think. Stan, can you confirm this is only an issue with the docs subdir? -benjamin > This is pretty tedious > when it happens to half the files in docs/html for instance. Could > we *please* not have id strings in the sources?