renamed to multithreading_dummy.ML;
authorwenzelm
Tue, 24 Jul 2007 19:46:44 +0200
changeset 23968091abf849a26
parent 23967 92130b24e87f
child 23969 ef782bbf2d09
renamed to multithreading_dummy.ML;
src/Pure/ML-Systems/no_multithreading.ML
     1.1 --- a/src/Pure/ML-Systems/no_multithreading.ML	Tue Jul 24 19:44:39 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,13 +0,0 @@
     1.4 -(*  Title:      Pure/ML-Systems/no_multithreading.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Compatibility file for ML systems without multithreading.
     1.9 -*)
    1.10 -
    1.11 -(*default number of worker threads*)
    1.12 -val multithreading = ref (NONE: int option);
    1.13 -
    1.14 -(*critical section*)
    1.15 -fun self_critical () = false;
    1.16 -fun CRITICAL e = e ();