-/** Compare two pointers (just to establish some sort of canonical order).
- * @return -1, 0, or 1 */
-int compare_pointers(const void * a, const void * b)
-{
- if (a<b) {
- return -1;
- } else if (a>b) {
- return 1;
- }
- return 0;
-}
-
-/** Append one exvector to another */
-void append_exvector_to_exvector(exvector & dest, const exvector & source)
-{
- dest.reserve(dest.size() + source.size());
- dest.insert(dest.end(), source.begin(), source.end());
-}
-