From 97cfecf5b5225a271518f616eb3936df5e204dac Mon Sep 17 00:00:00 2001 From: wolf Date: Tue, 1 Oct 2002 18:59:05 +0000 Subject: [PATCH] Remove old code. git-svn-id: https://svn.dealii.org/trunk@6585 0785d39b-7218-0410-832d-ea1e28bc413d --- deal.II/contrib/hsl/source/detached_ma27.cc | 17 ---------------- deal.II/lac/source/sparse_direct.cc | 22 --------------------- 2 files changed, 39 deletions(-) diff --git a/deal.II/contrib/hsl/source/detached_ma27.cc b/deal.II/contrib/hsl/source/detached_ma27.cc index 2d13382083..3e84c53e5a 100644 --- a/deal.II/contrib/hsl/source/detached_ma27.cc +++ b/deal.II/contrib/hsl/source/detached_ma27.cc @@ -27,12 +27,6 @@ #include #include -#ifdef HAVE_STD_STRINGSTREAM -# include -#else -# include -#endif - #ifndef DEAL_II_USE_DIRECT_ERRNO_H # include #else @@ -135,19 +129,8 @@ void die (const std::string &text, const T1 t1, const T2 t2) extern "C" void monitor_parent_liveness (const pid_t master_pid) { -// #ifdef HAVE_STD_STRINGSTREAM -// std::ostringstream s; -// s << "ps -p " << master_pid; -// const char * const command = s.str().c_str(); -// #else -// std::ostrstream s; -// s << "ps -p " << master_pid << std::ends; -// const char * const command = s.str(); -// #endif - while (true) { -// int ret = std::system (command); int ret = kill (master_pid, 0); if (ret != 0) if ((ret == -1) && (errno == ESRCH)) diff --git a/deal.II/lac/source/sparse_direct.cc b/deal.II/lac/source/sparse_direct.cc index 938fa204d7..932311b651 100644 --- a/deal.II/lac/source/sparse_direct.cc +++ b/deal.II/lac/source/sparse_direct.cc @@ -22,12 +22,6 @@ #include #include -#ifdef HAVE_STD_STRINGSTREAM -# include -#else -# include -#endif - #include #include #include @@ -313,24 +307,8 @@ void die (const std::string &text, const T1 t1, const T2 t2) extern "C" void monitor_child_liveness (const pid_t child_pid) { -// #ifdef HAVE_STD_STRINGSTREAM -// std::ostringstream s; -// s << "ps -p " << child_pid; -// const char * const command = s.str().c_str(); -// #else -// std::ostrstream s; -// s << "ps -p " << child_pid << std::ends; -// const char * const command = s.str(); -// #endif - while (true) { -// int ret = std::system (command); -// if (ret < 0) -// die ("Monitor process couldn't start 'ps'!"); -// else -// if (ret != 0) -// die ("Child process seems to have died!"); int ret = kill (child_pid, 0); if (ret != 0) if ((ret == -1) && (errno == ESRCH)) -- 2.39.5