From 19d0cbcd37003fa88ec4be3be9355263cf41da66 Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Tue, 1 Nov 2022 18:11:18 +0000 Subject: [PATCH] [ new ] put TTC files in a version-tagged directory (#2684) --- src/Compiler/Scheme/Chez.idr | 7 +-- src/Core/Context.idr | 2 +- src/Core/Directory.idr | 60 ++++++++++++++++++++---- src/Idris/Package.idr | 15 +++--- src/Idris/REPL.idr | 2 +- src/Idris/SetOptions.idr | 37 +++++---------- tests/Main.idr | 2 +- tests/chez/chez035/run | 2 +- tests/idris2/import008/Exe/Mod.idr | 6 +++ tests/idris2/import008/Exe/depends/lib-0 | 1 + tests/idris2/import008/Exe/exe.ipkg | 47 +++++++++++++++++++ tests/idris2/import008/Lib/Conf.idr | 7 +++ tests/idris2/import008/Lib/lib.ipkg | 47 +++++++++++++++++++ tests/idris2/import008/expected | 3 ++ tests/idris2/import008/run | 9 ++++ tests/idris2/pkg010/run | 2 +- tests/idris2/reg043/NotFake.idr | 1 + tests/idris2/reg043/expected | 1 + tests/idris2/reg043/run | 6 +-- tests/idris2/total012/run | 8 ++-- tests/templates/ttimp/run | 3 +- tests/ttimp/basic001/run | 3 +- tests/ttimp/basic003/run | 3 +- tests/ttimp/lazy001/run | 3 +- tests/ttimp/record001/run | 3 +- tests/ttimp/record003/run | 5 +- tests/ttimp/record004/run | 4 +- 27 files changed, 216 insertions(+), 73 deletions(-) create mode 100644 tests/idris2/import008/Exe/Mod.idr create mode 120000 tests/idris2/import008/Exe/depends/lib-0 create mode 100644 tests/idris2/import008/Exe/exe.ipkg create mode 100644 tests/idris2/import008/Lib/Conf.idr create mode 100644 tests/idris2/import008/Lib/lib.ipkg create mode 100644 tests/idris2/import008/expected create mode 100644 tests/idris2/import008/run create mode 100644 tests/idris2/reg043/NotFake.idr diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index f635fc01b..6bf419b53 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -218,8 +218,9 @@ loadSO : {auto c : Ref Ctxt Defs} -> loadSO appdir "" = pure "" loadSO appdir mod = do d <- getDirs - let fs = map (\p => p mod) - ((build_dir d "ttc") :: extra_dirs d) + bdir <- ttcBuildDirectory + allDirs <- extraSearchDirectories + let fs = map (\p => p mod) (bdir :: allDirs) Just fname <- firstAvailable fs | Nothing => throw (InternalError ("Missing .so:" ++ mod)) -- Easier to put them all in the same directory, so we don't need @@ -629,7 +630,7 @@ incCompile c s sourceFile cdata <- getIncCompileData False Cases d <- getDirs - let outputDir = build_dir d "ttc" + outputDir <- ttcBuildDirectory let ndefs = namedDefs cdata if isNil ndefs diff --git a/src/Core/Context.idr b/src/Core/Context.idr index d55a021b6..277bb6db7 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2088,7 +2088,7 @@ addExtraDir : {auto c : Ref Ctxt Defs} -> String -> Core () addExtraDir dir = update Ctxt { options->dirs->extra_dirs $= (++ [dir]) } export -addPackageDir : {auto c : Ref Ctxt Defs} -> String -> Core () +addPackageDir: {auto c : Ref Ctxt Defs} -> String -> Core () addPackageDir dir = update Ctxt { options->dirs->package_dirs $= (++ [dir]) } export diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 4d5e550e4..5f8305d86 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -1,13 +1,17 @@ module Core.Directory +import Core.Binary import Core.Context import Core.Context.Log import Core.Core import Core.FC import Core.Options +import Idris.Version + import Parser.Unlit +import Libraries.Data.Version import Libraries.Utils.Path import Data.List @@ -17,6 +21,46 @@ import System.Directory %default total +------------------------------------------------------------------------ +-- Package directories + +export +pkgGlobalDirectory : {auto c : Ref Ctxt Defs} -> Core String +pkgGlobalDirectory = + do d <- getDirs + pure (prefix_dir d "idris2-" ++ showVersion False version) + +export +pkgLocalDirectory : {auto c : Ref Ctxt Defs} -> Core String +pkgLocalDirectory = + do d <- getDirs + Just srcdir <- coreLift currentDir + | Nothing => throw (InternalError "Can't get current directory") + pure $ srcdir depends_dir d + +------------------------------------------------------------------------ +-- TTC directories + +export +ttcBuildDirectory : {auto c : Ref Ctxt Defs} -> Core String +ttcBuildDirectory = + do d <- getDirs + pure (build_dir d "ttc" show ttcVersion) + +export +ttcInstallDirectory : {auto c : Ref Ctxt Defs} -> String -> Core String +ttcInstallDirectory lib = + do gbdir <- pkgGlobalDirectory + pure (gbdir lib show ttcVersion) + +export +extraSearchDirectories : {auto c : Ref Ctxt Defs} -> Core (List String) +extraSearchDirectories = + do d <- getDirs + pure (map ( show ttcVersion) (extra_dirs d ++ package_dirs d)) + +------------------------------------------------------------------------ + public export data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md @@ -126,10 +170,10 @@ export nsToPath : {auto c : Ref Ctxt Defs} -> FC -> ModuleIdent -> Core (Either Error String) nsToPath loc ns - = do d <- getDirs + = do bdir <- ttcBuildDirectory + ttcs <- extraSearchDirectories let fnameBase = ModuleIdent.toPath ns - let fs = map (\p => cleanPath $ p fnameBase <.> "ttc") - ((build_dir d "ttc") :: extra_dirs d) + let fs = map (\p => cleanPath $ p fnameBase <.> "ttc") (bdir :: ttcs) Just f <- firstAvailable fs | Nothing => pure (Left (ModuleNotFound loc ns)) pure (Right f) @@ -207,12 +251,11 @@ covering makeBuildDirectory : {auto c : Ref Ctxt Defs} -> ModuleIdent -> Core () makeBuildDirectory ns - = do d <- getDirs - let bdir = build_dir d "ttc" + = do bdir <- ttcBuildDirectory let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name let ndir = joinPath ns Right _ <- coreLift $ mkdirAll (bdir ndir) - | Left err => throw (FileErr (build_dir d ndir) err) + | Left err => throw (FileErr (bdir ndir) err) pure () export @@ -232,9 +275,8 @@ getTTCFileName inp ext -- and generate the ttc file from that ns <- ctxtPathToNS inp let fname = ModuleIdent.toPath ns <.> ext - d <- getDirs - let bdir = build_dir d - pure $ bdir "ttc" fname + bdir <- ttcBuildDirectory + pure $ bdir fname -- Given a source file, return the name of the corresponding object file. -- As above, but without the build directory diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index f6dafe1e3..908462f63 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -357,7 +357,7 @@ addDeps pkg = do Resolved allPkgs <- getTransitiveDeps pkg.depends empty | Failed errs => throw $ GenericMsg EmptyFC (printErrs pkg errs) log "package.depends" 10 $ "all depends: \{show allPkgs}" - traverse_ addExtraDir allPkgs + traverse_ addPackageDir allPkgs where -- Note: findPkgDir throws an error if a package is not found -- *unless* --ignore-missing-ipkg is enabled @@ -487,14 +487,14 @@ installFrom : {auto o : Ref ROpts REPLOpts} -> String -> String -> ModuleIdent -> Core () installFrom builddir destdir ns = do let ttcfile = ModuleIdent.toPath ns - let ttcPath = builddir "ttc" ttcfile <.> "ttc" + let ttcPath = builddir ttcfile <.> "ttc" objPaths_in <- traverse (\cg => do Just cgdata <- getCG cg | Nothing => pure Nothing let Just ext = incExt cgdata | Nothing => pure Nothing - let srcFile = builddir "ttc" ttcfile <.> ext + let srcFile = builddir ttcfile <.> ext let destFile = destdir ttcfile <.> ext let Just (dir, _) = splitParent destFile | Nothing => pure Nothing @@ -574,7 +574,8 @@ install : {auto c : Ref Ctxt Defs} -> Core () install pkg opts installSrc -- not used but might be in the future = do defs <- get Ctxt - let build = build_dir (dirs (options defs)) + build <- ttcBuildDirectory + targetDir <- ttcInstallDirectory (installDir pkg) let src = source_dir (dirs (options defs)) runScript (preinstall pkg) let toInstall = maybe (modules pkg) @@ -582,9 +583,6 @@ install pkg opts installSrc -- not used but might be in the future (mainmod pkg) wdir <- getWorkingDir -- Make the package installation directory - let targetDir = prefix_dir (dirs (options defs)) - "idris2-" ++ showVersion False version - installDir pkg Right _ <- coreLift $ mkdirAll targetDir | Left err => throw $ InternalError $ unlines [ "Can't make directory " ++ targetDir @@ -785,7 +783,8 @@ clean pkg opts -- `opts` is not used but might be in the future pkgmods srcdir <- getWorkingDir let d = dirs (options defs) - let builddir = srcdir build_dir d "ttc" + bdir <- ttcBuildDirectory + let builddir = srcdir bdir "ttc" let outputdir = srcdir outputDirWithDefault d -- the usual pair syntax breaks with `No such variable a` here for some reason let pkgTrie : StringTrie (List String) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 448784b84..8f1ff9f2c 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -1074,7 +1074,7 @@ process ShowVersion = pure $ VersionIs version process (ImportPackage package) = do defs <- get Ctxt - let searchDirs = defs.options.dirs.extra_dirs + searchDirs <- extraSearchDirectories let Just packageDir = find (\d => isInfixOf package (fromMaybe d (fileName d))) searchDirs diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 3307d2ffc..5a60149fa 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -3,6 +3,7 @@ module Idris.SetOptions import Compiler.Common import Core.Context +import Core.Directory import Core.Metadata import Core.Options import Core.Unify @@ -76,20 +77,6 @@ candidateDirs dname pkg bounds = do guard (pkgName == pkg && inBounds ver bounds) pure ((dname dirName), ver) -globalPackageDir : {auto c : Ref Ctxt Defs} -> Core String -globalPackageDir - = do defs <- get Ctxt - pure $ prefix_dir (dirs (options defs)) - "idris2-" ++ showVersion False version - -localPackageDir : {auto c : Ref Ctxt Defs} -> Core String -localPackageDir - = do defs <- get Ctxt - Just srcdir <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") - let depends = depends_dir (dirs (options defs)) - pure $ srcdir depends - ||| Find all package directories (plus version) matching ||| the given package name and version bounds. Results ||| will be sorted with the latest package version first. @@ -100,17 +87,16 @@ findPkgDirs : PkgVersionBounds -> Core (List (String, Maybe PkgVersion)) findPkgDirs p bounds = do - defs <- get Ctxt - globaldir <- globalPackageDir - localdir <- localPackageDir + globaldir <- pkgGlobalDirectory + localdir <- pkgLocalDirectory -- Get candidate directories from the global install location, -- and the local package directory locFiles <- coreLift $ candidateDirs localdir p bounds globFiles <- coreLift $ candidateDirs globaldir p bounds -- Look in all the package paths too - let pkgdirs = (options defs).dirs.package_dirs - pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) pkgdirs + d <- getDirs + pkgFiles <- coreLift $ traverse (\d => candidateDirs d p bounds) (package_dirs d) -- If there's anything locally, use that and ignore the global ones let allFiles = if isNil locFiles @@ -142,7 +128,7 @@ addPkgDir : {auto c : Ref Ctxt Defs} -> addPkgDir p bounds = do Just p <- findPkgDir p bounds | Nothing => pure () - addExtraDir p + addPackageDir p visiblePackages : String -> IO (List PkgDir) visiblePackages dir = filter viable <$> getPackageDirs dir @@ -158,14 +144,13 @@ visiblePackages dir = filter viable <$> getPackageDirs dir findPackages : {auto c : Ref Ctxt Defs} -> Core (List PkgDir) findPackages = do -- global packages - defs <- get Ctxt - globalPkgs <- coreLift $ visiblePackages !globalPackageDir + globalPkgs <- coreLift $ visiblePackages !pkgGlobalDirectory -- additional packages in directories specified - let pkgDirs = (options defs).dirs.package_dirs - additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) pkgDirs + d <- getDirs + additionalPkgs <- coreLift $ traverse (\d => visiblePackages d) (package_dirs d) -- local packages - localPkgs <- coreLift $ visiblePackages !localPackageDir - pure $ globalPkgs ++ (join additionalPkgs) ++ localPkgs + localPkgs <- coreLift $ visiblePackages !pkgLocalDirectory + pure $ globalPkgs ++ join additionalPkgs ++ localPkgs listPackages : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> diff --git a/tests/Main.idr b/tests/Main.idr index 525afb13f..8a5adca67 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -261,7 +261,7 @@ idrisTests = MkTestPool "Misc" [] Nothing "eta001", -- Modules and imports "import001", "import002", "import003", "import004", "import005", "import006", - "import007", + "import007", "import008", -- Implicit laziness, lazy evaluation "lazy001", "lazy002", -- Namespace blocks diff --git a/tests/chez/chez035/run b/tests/chez/chez035/run index 099e6ea04..895d856e6 100755 --- a/tests/chez/chez035/run +++ b/tests/chez/chez035/run @@ -5,6 +5,6 @@ export IDRIS2_INC_CGS=chez $1 --no-banner --no-color --console-width 0 -o test Mod2.idr < input ./build/exec/test -ls build/ttc/Mod1.so +ls build/ttc/*/Mod1.so | sed -r "s/.([0-9]){10}//g" rm -rf build diff --git a/tests/idris2/import008/Exe/Mod.idr b/tests/idris2/import008/Exe/Mod.idr new file mode 100644 index 000000000..6ecf636c4 --- /dev/null +++ b/tests/idris2/import008/Exe/Mod.idr @@ -0,0 +1,6 @@ +module Mod + +import Conf + +main : IO () +main = putStrLn msg diff --git a/tests/idris2/import008/Exe/depends/lib-0 b/tests/idris2/import008/Exe/depends/lib-0 new file mode 120000 index 000000000..a97ac90c8 --- /dev/null +++ b/tests/idris2/import008/Exe/depends/lib-0 @@ -0,0 +1 @@ +../../Lib/build/ttc/ \ No newline at end of file diff --git a/tests/idris2/import008/Exe/exe.ipkg b/tests/idris2/import008/Exe/exe.ipkg new file mode 100644 index 000000000..7bdd7fdff --- /dev/null +++ b/tests/idris2/import008/Exe/exe.ipkg @@ -0,0 +1,47 @@ +package exe +-- version = +-- authors = +-- maintainers = +-- license = +-- brief = +-- readme = +-- homepage = +-- sourceloc = +-- bugtracker = + +-- the Idris2 version required (e.g. langversion >= 0.5.1) +-- langversion + +-- packages to add to search path +depends = lib + +-- modules to install +modules = Mod + +-- main file (i.e. file to load at REPL) +-- main = + +-- name of executable +-- executable = +-- opts = +-- sourcedir = +-- builddir = +-- outputdir = + +-- script to run before building +-- prebuild = + +-- script to run after building +-- postbuild = + +-- script to run after building, before installing +-- preinstall = + +-- script to run after installing +-- postinstall = + +-- script to run before cleaning +-- preclean = + +-- script to run after cleaning +-- postclean = diff --git a/tests/idris2/import008/Lib/Conf.idr b/tests/idris2/import008/Lib/Conf.idr new file mode 100644 index 000000000..9c75bbd3e --- /dev/null +++ b/tests/idris2/import008/Lib/Conf.idr @@ -0,0 +1,7 @@ +module Conf + +%default total + +export +msg : String +msg = "hello world" diff --git a/tests/idris2/import008/Lib/lib.ipkg b/tests/idris2/import008/Lib/lib.ipkg new file mode 100644 index 000000000..598b46022 --- /dev/null +++ b/tests/idris2/import008/Lib/lib.ipkg @@ -0,0 +1,47 @@ +package lib +-- version = +-- authors = +-- maintainers = +-- license = +-- brief = +-- readme = +-- homepage = +-- sourceloc = +-- bugtracker = + +-- the Idris2 version required (e.g. langversion >= 0.5.1) +-- langversion + +-- packages to add to search path +-- depends = + +-- modules to install +modules = Conf + +-- main file (i.e. file to load at REPL) +-- main = + +-- name of executable +-- executable = +-- opts = +-- sourcedir = +-- builddir = +-- outputdir = + +-- script to run before building +-- prebuild = + +-- script to run after building +-- postbuild = + +-- script to run after building, before installing +-- preinstall = + +-- script to run after installing +-- postinstall = + +-- script to run before cleaning +-- preclean = + +-- script to run after cleaning +-- postclean = \ No newline at end of file diff --git a/tests/idris2/import008/expected b/tests/idris2/import008/expected new file mode 100644 index 000000000..e5f87309c --- /dev/null +++ b/tests/idris2/import008/expected @@ -0,0 +1,3 @@ +1/1: Building Conf (Conf.idr) +1/1: Building Mod (Mod.idr) +hello world diff --git a/tests/idris2/import008/run b/tests/idris2/import008/run new file mode 100644 index 000000000..5b11a405e --- /dev/null +++ b/tests/idris2/import008/run @@ -0,0 +1,9 @@ +rm -rf Exe/build +rm -rf Lib/build + +cd Lib +$1 --build +cd .. +cd Exe +$1 --no-color --console-width 0 --no-banner --check --find-ipkg Mod.idr +$1 --no-color --console-width 0 --no-banner --exec main --find-ipkg Mod.idr diff --git a/tests/idris2/pkg010/run b/tests/idris2/pkg010/run index 2ca608185..ebaa47731 100755 --- a/tests/idris2/pkg010/run +++ b/tests/idris2/pkg010/run @@ -11,7 +11,7 @@ export IDRIS2_PREFIX=${MY_PWD}currently/nonexistent/dir/ export IDRIS2_INC_CGS= -$1 --install ./testpkg.ipkg +$1 --install ./testpkg.ipkg | sed -r "s/.([0-9]){10}//g" # ../ is there for some extra safety for using rm -rf rm -rf ../pkg010/build ../pkg010/currently diff --git a/tests/idris2/reg043/NotFake.idr b/tests/idris2/reg043/NotFake.idr new file mode 100644 index 000000000..1aebc6c61 --- /dev/null +++ b/tests/idris2/reg043/NotFake.idr @@ -0,0 +1 @@ +module NotFake diff --git a/tests/idris2/reg043/expected b/tests/idris2/reg043/expected index 50c05918f..83491f6b9 100644 --- a/tests/idris2/reg043/expected +++ b/tests/idris2/reg043/expected @@ -1,2 +1,3 @@ +1/1: Building NotFake (NotFake.idr) 1/1: Building TestFake (TestFake.idr) Error: Error in TTC file: Corrupt TTC data for String (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files) diff --git a/tests/idris2/reg043/run b/tests/idris2/reg043/run index f18707b76..48f91c057 100755 --- a/tests/idris2/reg043/run +++ b/tests/idris2/reg043/run @@ -1,7 +1,7 @@ rm -rf build -mkdir -p build/ttc -echo "TT2This Is A Fake TTC" > build/ttc/Fake.ttc +$1 --no-color --console-width 0 --check NotFake.idr + +echo "TT2This Is A Fake TTC" > build/ttc/$(ls build/ttc)/Fake.ttc $1 --no-color --console-width 0 --check TestFake.idr - diff --git a/tests/idris2/total012/run b/tests/idris2/total012/run index 1ded15733..9ce204c22 100755 --- a/tests/idris2/total012/run +++ b/tests/idris2/total012/run @@ -1,12 +1,12 @@ rm -rf build $1 --no-color --console-width 0 Issue1828.idr --check -$1 --no-color --console-width 0 Issue1828.idr --check --total --log totality.requirement:20 +$1 --no-color --console-width 0 Issue1828.idr --check --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" $1 --no-color --console-width 0 Issue1828.idr --check -$1 --no-color --console-width 0 Issue1828.idr --check --log totality.requirement:20 +$1 --no-color --console-width 0 Issue1828.idr --check --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" $1 --no-color --console-width 0 TotallyTotal.idr --check -$1 --no-color --console-width 0 TotallyTotal.idr --check --log totality.requirement:20 -$1 --no-color --console-width 0 TotallyTotal.idr --check --total --log totality.requirement:20 \ No newline at end of file +$1 --no-color --console-width 0 TotallyTotal.idr --check --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" +$1 --no-color --console-width 0 TotallyTotal.idr --check --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" \ No newline at end of file diff --git a/tests/templates/ttimp/run b/tests/templates/ttimp/run index 0e705f540..d7e98d283 100755 --- a/tests/templates/ttimp/run +++ b/tests/templates/ttimp/run @@ -1,5 +1,4 @@ rm -rf build $1 --yaffle Interp.yaff < input -$1 --yaffle build/ttc/Interp.ttc < input - +$1 --yaffle build/ttc/$(ls build/ttc/)/Interp.ttc < input diff --git a/tests/ttimp/basic001/run b/tests/ttimp/basic001/run index 0e705f540..ce479ad0d 100755 --- a/tests/ttimp/basic001/run +++ b/tests/ttimp/basic001/run @@ -1,5 +1,4 @@ rm -rf build $1 --yaffle Interp.yaff < input -$1 --yaffle build/ttc/Interp.ttc < input - +$1 --yaffle build/ttc/*/Interp.ttc < input diff --git a/tests/ttimp/basic003/run b/tests/ttimp/basic003/run index b80000004..390f21773 100755 --- a/tests/ttimp/basic003/run +++ b/tests/ttimp/basic003/run @@ -1,5 +1,4 @@ rm -rf build $1 --yaffle Hole.yaff < input -$1 --yaffle build/ttc/Hole.ttc < input - +$1 --yaffle build/ttc/*/Hole.ttc < input diff --git a/tests/ttimp/lazy001/run b/tests/ttimp/lazy001/run index 7355a5616..bd5cc7c9f 100755 --- a/tests/ttimp/lazy001/run +++ b/tests/ttimp/lazy001/run @@ -2,5 +2,4 @@ rm -rf build $1 --yaffle Lazy.yaff < input $1 --yaffle LazyInf.yaff < input -$1 --yaffle build/ttc/LazyInf.ttc < input - +$1 --yaffle build/ttc/*/LazyInf.ttc < input diff --git a/tests/ttimp/record001/run b/tests/ttimp/record001/run index c22772cde..afcde9aeb 100755 --- a/tests/ttimp/record001/run +++ b/tests/ttimp/record001/run @@ -1,5 +1,4 @@ rm -rf build $1 --yaffle Record.yaff < input -$1 --yaffle build/ttc/Record.ttc < input - +$1 --yaffle build/ttc/*/Record.ttc < input diff --git a/tests/ttimp/record003/run b/tests/ttimp/record003/run index cc4093fb1..afcde9aeb 100755 --- a/tests/ttimp/record003/run +++ b/tests/ttimp/record003/run @@ -1,5 +1,4 @@ rm -rf build -$1 --yaffle Record.yaff < input -$1 --yaffle build/ttc/Record.ttc < input - +$1 --yaffle Record.yaff < input +$1 --yaffle build/ttc/*/Record.ttc < input diff --git a/tests/ttimp/record004/run b/tests/ttimp/record004/run index 2df237b7e..afcde9aeb 100644 --- a/tests/ttimp/record004/run +++ b/tests/ttimp/record004/run @@ -1,4 +1,4 @@ rm -rf build -$1 --yaffle Record.yaff < input -$1 --yaffle build/ttc/Record.ttc < input +$1 --yaffle Record.yaff < input +$1 --yaffle build/ttc/*/Record.ttc < input