Fixes for record deletion bug, and optimization
Record deletion was broken on the VPN db, and it turned out it was because it was timing out because the project_settings.php file was not being included in del_rec.php, so the time required to do the deletion was running over the default time for PHP requests. However, having fixed that, I decided that the way del_rec.php was behaving made no sense anyway; after deleting a record, it made a whole fresh request to the db for its first set of records and replaced the existing table with that. Instead, it now returns a simple OK, and the JS code instead calls a function which deletes the two table rows associated with the deleted record, leaving the rest of the stuff intact. That's much quicker and more intuitive.
A similar process was required for multi-record editing. At first I thought this was going to be really complicated, but it turned out that since all the search filter data is being sent along with the editing data as part of the query, it's sufficient just to include the regular get_search_results.php file at the required point, causing the current search query to be re-run and the modified results returned. Looks like it works perfectly; we'll see if there are any reports of errors.