Today, the indexing for the main website is driven off the same sitemap.xml that we feed Google. And we did at some point in the past (quite long ago) decide we didn't want /devel/ to be included in the Google search hits.
We probably want to include them in our own, at least when you are explicitly searching in that subsection. That will require some code changes to make it happy with that though - we'd have to send out a separate sitemap.xml to our own search engine.
Or is there a change in the consensus that we should not have Google return search hits of that?
